Peng Fu

Publication Activity (10 Years)

Years Active: 2012-2023
Publications (10 Years): 19

Top Topics

Operational Semantics

Automatic Theorem Proving

Horn Clause Logic

Quantum Mechanics

Top Venues

Proc. ACM Program. Lang.

J. Funct. Program.

Publications

Peng Fu, Peter Selinger
Towards an Induction Principle for Nested Data Types. WoLLIC (2023)
Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger
Proto-Quipper with Dynamic Lifting. Proc. ACM Program. Lang. 7 (POPL) (2023)
Peng Fu, Peter Selinger
Towards an induction principle for nested data types. CoRR (2023)
Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger
On the Lambek embedding and the category of product-preserving presheaves. CoRR (2022)
Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger
Proto-Quipper with dynamic lifting. CoRR (2022)
Peng Fu, Kohei Kishida, Peter Selinger
Linear Dependent Type Theory for Quantum Programming Languages. Log. Methods Comput. Sci. 18 (3) (2022)
Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger
A biset-enriched categorical model for Proto-Quipper with dynamic lifting. CoRR (2022)
Peng Fu, Kohei Kishida, Peter Selinger
Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract. LICS (2020)
Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger
A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper. RC (2020)
Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger
A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper. CoRR (2020)
Peng Fu, Kohei Kishida, Peter Selinger
Linear Dependent Type Theory for Quantum Programming Languages. CoRR (2020)
Peng Fu, Peter Selinger
Dependently Typed Folds for Nested Data Types. CoRR (2018)
Peng Fu
. CoRR (2017)
Peng Fu, Ekaterina Komendantskaya
Operational semantics of resolution and productivity in Horn clause logic. Formal Aspects Comput. 29 (3) (2017)
Peng Fu
A Type Checking Algorithm for Higher-rank, Impredicative and Second-order Types. CoRR (2017)
Frantisek Farka, Ekaterina Komendantskaya, Kevin Hammond, Peng Fu
Coinductive Soundness of Corecursive Type Class Resolution. CoRR (2016)
Aaron Stump, Peng Fu
Efficiency of lambda-encodings in total type theory. J. Funct. Program. 26 (2016)
Peng Fu, Ekaterina Komendantskaya
Operational Semantics of Resolution in Horn Clause Logic. CoRR (2016)
Peng Fu, Ekaterina Komendantskaya, Tom Schrijvers, Andrew Pond
Proof Relevant Corecursive Resolution. FLOPS (2016)
Peng Fu, Ekaterina Komendantskaya, Tom Schrijvers, Andrew Pond
Proof Relevant Corecursive Resolution. CoRR (2015)
Peng Fu, Ekaterina Komendantskaya
A Type-Theoretic Approach to Resolution. LOPSTR (2015)
Peng Fu, Ekaterina Komendantskaya
A Type-Theoretic Approach to Resolution. CoRR (2015)
Peng Fu, Ekaterina Komendantskaya
A Type-Theoretic Approach to Structural Resolution. CoRR (2015)
Peng Fu, Aaron Stump
Self Types for Dependently Typed Lambda Encodings. RTA-TLCA (2014)
Garrin Kimmell, Aaron Stump, Harley D. Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathan Collins, Ki Yung Ahn
Equational reasoning about programs with general recursion and call-by-value semantics. PLPV (2012)
Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich
Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems MSFP (2012)