Follow
Peng Fu
Title
Cited by
Cited by
Year
Proof relevant corecursive resolution
P Fu, E Komendantskaya, T Schrijvers, A Pond
Functional and Logic Programming: 13th International Symposium, FLOPS 2016 …, 2016
342016
Equational reasoning about programs with general recursion and call-by-value semantics
G Kimmell, A Stump, HD Eades III, P Fu, T Sheard, S Weirich, ...
Proceedings of the sixth workshop on Programming languages meets program …, 2012
322012
Irrelevance, heterogeneous equality, and call-by-value dependent type systems
V Sjöberg, C Casinghino, KY Ahn, N Collins, HD Eades III, P Fu, ...
arXiv preprint arXiv:1202.2923, 2012
302012
Linear dependent type theory for quantum programming languages
P Fu, K Kishida, P Selinger
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer …, 2020
272020
Operational semantics of resolution and productivity in Horn clause logic
P Fu, E Komendantskaya
Formal Aspects of Computing 29, 453-474, 2017
262017
A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper
P Fu, K Kishida, NJ Ross, P Selinger
Reversible Computation: 12th International Conference, RC 2020, Oslo, Norway …, 2020
192020
Self types for dependently typed lambda encodings
P Fu, A Stump
Rewriting and Typed Lambda Calculi: Joint International Conference, RTA-TLCA …, 2014
132014
A type-theoretic approach to resolution
P Fu, E Komendantskaya
Logic-Based Program Synthesis and Transformation: 25th International …, 2015
122015
Efficiency of lambda-encodings in total type theory
A Stump, P Fu
Journal of functional programming 26, e3, 2016
102016
A biset-enriched categorical model for Proto-Quipper with dynamic lifting
P Fu, K Kishida, NJ Ross, P Selinger
arXiv preprint arXiv:2204.13039, 2022
62022
Proto-Quipper with dynamic lifting
P Fu, K Kishida, NJ Ross, P Selinger
arXiv preprint arXiv:2204.13041, 2022
52022
Dependently typed folds for nested data types
P Fu, P Selinger
arXiv preprint arXiv:1806.05230, 2018
22018
A type-theoretic approach to structural resolution
P Fu, E Komendantskaya
arXiv preprint arXiv:1506.06166, 2015
22015
Horn Formulas as Types for Structural Resolution
P Fu, E Komendantskaya
LOPSTR, 2015
22015
A framework for internalizing relations into type theory
P Fu, A Stump, J Vaughan
PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and …, 2011
22011
Church encoding with dependent types
P Fu, A Stump
12013
Linear Dependent Type Theory for Quantum Programming Languages
P Selinger, K Kishida, P Fu
Logical Methods in Computer Science 18, 2022
2022
On the Lambek embedding and the category of product-preserving presheaves
P Fu, K Kishida, NJ Ross, P Selinger
arXiv preprint arXiv:2205.06068, 2022
2022
Representing Nonterminating Rewriting with
P Fu
arXiv preprint arXiv:1706.00746, 2017
2017
Operational Semantics of Resolution in Horn Clause Logic
P Fu, E Komendantskaya
arXiv preprint arXiv:1604.04114, 2016
2016
The system can't perform the operation now. Try again later.
Articles 1–20