Peng Fu

According to our database, Peng Fu authored at least 20 papers between 2012 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2023

Proto-Quipper with Dynamic Lifting.

Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger

Proc. ACM Program. Lang., January, 2023

Towards an Induction Principle for Nested Data Types.

Peng Fu, Peter Selinger

Proceedings of the Logic, Language, Information, and Computation, 2023

2022

Linear Dependent Type Theory for Quantum Programming Languages.

Peng Fu, Kohei Kishida, Peter Selinger

Log. Methods Comput. Sci., 2022

On the Lambek embedding and the category of product-preserving presheaves.

Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger

CoRR, 2022

A biset-enriched categorical model for Proto-Quipper with dynamic lifting.

Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger

Proceedings of the Proceedings 19th International Conference on Quantum Physics and Logic, 2022

2020

A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper.

Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger

Proceedings of the Reversible Computation - 12th International Conference, 2020

Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract.

Peng Fu, Kohei Kishida, Peter Selinger

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

2018

Dependently Typed Folds for Nested Data Types.

Peng Fu, Peter Selinger

CoRR, 2018

2017

Operational semantics of resolution and productivity in Horn clause logic.

Peng Fu, Ekaterina Komendantskaya

Formal Aspects Comput., 2017

A Type Checking Algorithm for Higher-rank, Impredicative and Second-order Types.

Peng Fu

CoRR, 2017

Representing Nonterminating Rewriting with F₂^μ.

Peng Fu

CoRR, 2017

2016

Efficiency of lambda-encodings in total type theory.

Aaron Stump, Peng Fu

J. Funct. Program., 2016

Coinductive Soundness of Corecursive Type Class Resolution.

Frantisek Farka, Ekaterina Komendantskaya, Kevin Hammond, Peng Fu

CoRR, 2016

Operational Semantics of Resolution in Horn Clause Logic.

Peng Fu, Ekaterina Komendantskaya

CoRR, 2016

Proof Relevant Corecursive Resolution.

Peng Fu, Ekaterina Komendantskaya, Tom Schrijvers, Andrew Pond

Proceedings of the Functional and Logic Programming - 13th International Symposium, 2016

2015

A Type-Theoretic Approach to Structural Resolution.

Peng Fu, Ekaterina Komendantskaya

CoRR, 2015

A Type-Theoretic Approach to Resolution.

Peng Fu, Ekaterina Komendantskaya

Proceedings of the Logic-Based Program Synthesis and Transformation, 2015

2014

Self Types for Dependently Typed Lambda Encodings.

Peng Fu, Aaron Stump

Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

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, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich

Proceedings of the Proceedings Fourth Workshop on Mathematically Structured Functional Programming, 2012

Equational reasoning about programs with general recursion and call-by-value semantics.

Garrin Kimmell, Aaron Stump, Harley D. Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathan Collins, Ki Yung Ahn

Proceedings of the sixth workshop on Programming Languages meets Program Verification, 2012