Equational reasoning about programs with general recursion and call-by-value semantics. - Garrin Kimmell; Aaron Stump; Harley D. Eades III; Peng Fu 001; Tim Sheard; Stephanie Weirich; Chris Casinghino; Vilhelm Sjöberg; Nathan Collins; Ki Yung Ahn (PLPV, 2012)

Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems - Vilhelm Sjöberg; Chris Casinghino; Ki Yung Ahn; Nathan Collins; Harley D. Eades III; Peng Fu 001; Garrin Kimmell; Tim Sheard; Aaron Stump; Stephanie Weirich (MSFP, 2012)

Self Types for Dependently Typed Lambda Encodings. - Peng Fu 001; Aaron Stump (RTA-TLCA, 2014)

A Type-Theoretic Approach to Resolution. - Peng Fu 001; Ekaterina Komendantskaya (LOPSTR, 2015)

A Type-Theoretic Approach to Structural Resolution. - Peng Fu 001; Ekaterina Komendantskaya (CoRR, 2015)

Proof Relevant Corecursive Resolution. - Peng Fu 001; Ekaterina Komendantskaya; Tom Schrijvers; Andrew Pond (FLOPS, 2016)

Operational Semantics of Resolution in Horn Clause Logic. - Peng Fu 001; Ekaterina Komendantskaya (CoRR, 2016)

Coinductive Soundness of Corecursive Type Class Resolution. - Frantisek Farka; Ekaterina Komendantskaya; Kevin Hammond; Peng Fu 001 (CoRR, 2016)

Efficiency of lambda-encodings in total type theory. - Aaron Stump; Peng Fu 001 (J. Funct. Program., 2016)

Representing Nonterminating Rewriting with F2μ. - Peng Fu 001 (CoRR, 2017)

A Type Checking Algorithm for Higher-rank, Impredicative and Second-order Types. - Peng Fu 001 (CoRR, 2017)

Operational semantics of resolution and productivity in Horn clause logic. - Peng Fu 001; Ekaterina Komendantskaya (Formal Aspects Comput., 2017)

Dependently Typed Folds for Nested Data Types. - Peng Fu 001; Peter Selinger (CoRR, 2018)

Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract. - Peng Fu 001; Kohei Kishida; Peter Selinger (LICS, 2020)

A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper. - Peng Fu 001; Kohei Kishida; Neil J. Ross; Peter Selinger (RC, 2020)

A biset-enriched categorical model for Proto-Quipper with dynamic lifting. - Peng Fu 001; Kohei Kishida; Neil J. Ross; Peter Selinger (QPL, 2022)

On the Lambek embedding and the category of product-preserving presheaves. - Peng Fu 001; Kohei Kishida; Neil J. Ross; Peter Selinger (CoRR, 2022)

Linear Dependent Type Theory for Quantum Programming Languages. - Peng Fu 001; Kohei Kishida; Peter Selinger (Log. Methods Comput. Sci., 2022)

Towards an Induction Principle for Nested Data Types. - Peng Fu 001; Peter Selinger (WoLLIC, 2023)

Proto-Quipper with Dynamic Lifting. - Peng Fu 001; Kohei Kishida; Neil J. Ross; Peter Selinger (Proc. ACM Program. Lang., 2023)

Proto-Quipper with Reversing and Control. - Peng Fu 001; Kohei Kishida; Neil J. Ross; Peter Selinger (CoRR, 2024)