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
51 2020 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
37 2012 Proof relevant corecursive resolution P Fu, E Komendantskaya, T Schrijvers, A Pond
Functional and Logic Programming: 13th International Symposium, FLOPS 2016 …, 2016
35 2016 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
35 2012 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
30 2020 Operational semantics of resolution and productivity in Horn clause logic P Fu, E Komendantskaya
Formal Aspects of Computing 29, 453-474, 2017
27 2017 Proto-Quipper with dynamic lifting P Fu, K Kishida, NJ Ross, P Selinger
Proceedings of the ACM on Programming Languages 7 (POPL), 309-334, 2023
25 * 2023 Self types for dependently typed lambda encodings P Fu, A Stump
International Conference on Rewriting Techniques and Applications, 224-239, 2014
15 2014 A type-theoretic approach to resolution P Fu, E Komendantskaya
Logic-Based Program Synthesis and Transformation: 25th International …, 2015
13 2015 Efficiency of lambda-encodings in total type theory A Stump, P Fu
Journal of functional programming 26, e3, 2016
12 2016 Dependently typed folds for nested data types P Fu, P Selinger
arXiv preprint arXiv:1806.05230, 2018
2 2018 A type-theoretic approach to structural resolution P Fu, E Komendantskaya
arXiv preprint arXiv:1506.06166, 2015
2 2015 Horn Formulas as Types for Structural Resolution P Fu, E Komendantskaya
LOPSTR, 2015
2 2015 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
2 2011 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
1 2022 Church encoding with dependent types P Fu, A Stump
1 2013 Proto-Quipper with Reversing and Control P Fu, K Kishida, NJ Ross, P Selinger
arXiv preprint arXiv:2410.22261, 2024
2024 Towards an induction principle for nested data types P Fu, P Selinger
International Workshop on Logic, Language, Information, and Computation, 244-255, 2023
2023 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 