Peng Fu

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