Broadly speaking, I am interested in type theories and their applications in programming languages. In the past, I worked on supporting the verification of lambda-encoded programs in a type system and in a higher-order logic. I also enjoyed working on Haskell-style type class, which leads to a connection to term rewriting. I was excited to discover that we can verify and program with nested data types in a total programming language with dependent types. Recently, I am working on the design and implementation of a linear dependently typed system for quantum programming language, see a tutorial here. I am on the job market right now, have a look at my CV!
Linear Dependent Type Theory for Quantum Programming Languages. Peng Fu, Kohei Kishida, Peter Selinger, 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020. [arXiv]
A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper. Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger, 12th International Conference on Reversible Computation, 2020. [arXiv]
Dependently typed folds for nested data types. Peng Fu, Peter Selinger, 2018. [arXiv]
A Type Checking Algorithm for Higher-rank, Impredicative and Second-order Types. Peng Fu, 2017. [arXiv]
Representing Nonterminating Rewriting with $\mathbf{F}^2_{\mu}$. Peng Fu, 2017. [arXiv]
Efficiency of Lambda-Encodings in Total Type Theory. Aaron Stump, Peng Fu. Journal of Functional Programming, 2016. [pdf]
Proof Relevant Corecursive Resolution. Peng Fu, Ekaterina Komendantskaya, Tom Schrijvers, Andrew Pond. International Symposium on Functional and Logic Programming, 2016. [pdf]
Operational Semantics of Resolution and Productivity in Horn Clause Logic. Peng Fu, Ekaterina Komendantskaya. Formal Aspect of Computing, 2016 [pdf]
A Type-Theoretic Approach to Resolution. Peng Fu, Ekaterina Komendantskaya. International Symposium on Logic-Based Program Synthesis and Transformation, 2015. [pdf]
Lambda Encodings in Type Theory. Peng Fu, Dissertation, 2014. [pdf]
Self Types for Dependently Typed Lambda Encodings. Peng Fu, Aaron Stump. Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications, 2014. [pdf]
Equational Reasoning about Programs with General Recursion and Call-by-value Semantics. Garrin Kimmell, Aaron Stump, Harley Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjoberg, Nathan Collins, Ki Yung Ahn. Programming Languages meets Program Verification, 2012.
Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems. Vilhelm Sjoberg,Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich. Mathematically Structured Functional Programming, 2012.
A Framework for Internalizing Relations into Type Theory. Peng Fu, Aaron Stump, Jeff Vaughan. International Workshop on Proof-Search in Axiomatic Theories and Type Theories, 2011. [pdf]
Summary: Dependently typed Proto-Quipper is language for programming quantum circuits. It is an on-going project, one of the goals for this project is to make a type safe version of Quipper. We have implemented an prototype for this language. The main features include linear and dependent types. Linear types ensure the no-cloning property, while dependent types make programming circuit more natural.
Summary: This project shows how to program with nested data types in the total dependently typed language Agda using a new construct called dependently typed fold. We show how to derive induction principles for nested data types as well, hence enabling the verification of programs within Agda. As a case study, we translated all of the programs described by Ricard Bird and Ross Patterson's paper "De Bruijn notation as nested datatype" into Agda and prove their correctness within Agda. The Agda code is available in the project link above. The paper documentation explains the idea of the dependently typed folds and how to verify programs using the induction principles derived from the dependently typd folds.
Summary: Hindley-Milner type checking algorithm is widely used to implment mordern type checker. However, Hindley-Milner algorithm does not support higher-rank types. In presence of higher-rank, impredicative and higher-order types, it is often needed to annotate a program with types. In this project, we explore a type checking algorithm for higher-rank, impredicative and second-order types. The algorithm only requires type annotation at the top level, there is no need to annotate types inside a program. Compare to the popular bidirectional type checking algorithm, our type checking algorithm is based on resolution, which is a widely used technique in automated theorem proving. The algorithm is one direction, i.e. there is no type infer process, a program will always be checked against a certain type. As a case study, we implement a prototype type checker and use it to type check some nontrivial algorithms that makes essential use of impredicativity and second-order types, these include Stump's Church-encoded merge-sort(see here), Bird and Patterson's generalized folds(see here).
Summary: The Gottlob theorem prover implements a version of minimal higher-order logic and an interpretor for a polymorphic function programming language. The functional programs are translated to Scott-encoded lambda terms and the minimal higher-order logic uses comprehension principle to derive induction principle to reason about programs. As a case study, we use Gottlob to prove the correctness of the natural number division. It is unusual in the sense that the division algorithm will diverge when one of the input is zero(see here). This contracts the traditional theorem provers where all functions are requires to be terminating.
Remarks:
Remarks:
Linear dependent types for quantum circuit programming, February 17, 2020, PL Reading Group, University of Maryland, College Park, Maryland, USA. [Slides]
Dependent types in Proto-quipper, September 20, 2018, Dagstuhl Seminar: Quantum Programming Languages, Dagstuhl, Germany.
Encoding Data in Lambda Calculus: An Introduction, September 26, 2017, Atlantic Category Seminar, Dalhousie University, Canada. [Slides]
Proof Relevant Corecursive Resolution, June 22, 2016, The Scottish Programming Languages Seminar, Heriot-Watt University, Edinburgh, UK. [Slides]
A Type-Theoretic Approach to Structural Resolution, July 13, 2015, LOPSTR, Siena, Italy. [Slides]
Self Types for Dependently Typed Lambda Encodings, July 15, 2014, RTA-TLCA, Vienna, Austria. [Slides]
Lambda Encodings in Type Theory, May 2, 2014, Dissertation Defense, Iowa City, Iowa. [Slides]
Dependent Lambda Encoding with Self Types, September 2013, ACM SIGPLAN Workshop on Dependently-Typed Programming(DTP), Boston, MA. [Slides]
A Framework for Internalizing Relations into Type Theory, August 2011, PSATTT workshop, Wroclaw. Poland. [Slides]
Reducibility Method for Call-by-Value Simply Typed Lambda Calculus, March 2010. [pdf]
Subtyping Relation as Reducibility Set Inclusion, March 2010. [pdf]
Reducibility Method for Call-by-Value System $\mathbf{F}$, June 2010. [pdf]
Type Preservation for System $\mathbf{F}$ a la Curry, 2011. [pdf]
Confluence for Local Lambda-Mu Calculus, July 2013. [pdf]
Type Preservation for Curry Style $\mathbf{F}_{\omega}$, July 2013. [pdf]
Remarks: This note straightforwardly extends the method(by Barendregt) of proving type preservation for Curry style System $\mathbf{F}$ to $\mathbf{F}_{\omega}$
Lambda Encoding, Types and Confluence. [pdf]
Peng Fu. May 2013.
Remarks: This is my comprehensive exam paper.
Dependently-typed Programming with Scott Encoding. Peng Fu, Aaron Stump. 2013. [pdf]
Lambda Encoding with Comprehension. [pdf]
Peng Fu. Oct 2013.
Remarks: A Chapter from my dissertation.
Type Class and Logic Programming with Term Matching, Nov 2014. [pdf]
Remarks: This note shows how one can have a notion of logic programming based solely on term matching.
Realizability at work, June, 2017. [pdf]
Remarks: This notes shows examples of realization by termination and realization by shape index.