Proof relevant corecursive resolution P Fu, E Komendantskaya, T Schrijvers, A Pond International Symposium on Functional and Logic Programming, 126-143, 2016 | 33 | 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 | 31 | 2012 |

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 | 30 | 2012 |

Operational semantics of resolution and productivity in Horn clause logic P Fu, E Komendantskaya Formal Aspects of Computing 29 (3), 453-474, 2017 | 25 | 2017 |

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 | 17 | 2020 |

Self types for dependently typed lambda encodings P Fu, A Stump Rewriting and Typed Lambda Calculi, 224-239, 2014 | 13 | 2014 |

A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper P Fu, K Kishida, NJ Ross, P Selinger International Conference on Reversible Computation, 153-168, 2020 | 11 | 2020 |

A type-theoretic approach to resolution P Fu, E Komendantskaya International Symposium on Logic-Based Program Synthesis and Transformation …, 2015 | 11 | 2015 |

Efficiency of lambda-encodings in total type theory A Stump, P Fu Journal of functional programming 26, 2016 | 10 | 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 |

Proto-Quipper with dynamic lifting P Fu, K Kishida, NJ Ross, P Selinger arXiv preprint arXiv:2204.13041, 2022 | 1 | 2022 |

Church encoding with dependent types P Fu, A Stump | 1 | 2013 |

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 |

Lambda encodings in type theory P Fu The University of Iowa, 2014 | | 2014 |

Lambda Encoding with Comprehension P Fu | | 2013 |