Broadly speaking, I am interested in type theories and their applications in
programming languages.
I am working on the design and implementation of a linear
dependently typed system for quantum programming language,
see a tutorial here.
I am also organizing
the ATCAT seminar this semester, here is the current schedule.
Peng Fu, Kohei Kishida, Peter Selinger, 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020. [pdf] [talk]
Remarks: Invited for submission to special issue of Logical Methods in Computer Science (LMCS) devoted to selected papers from LICS 2020. Submission available at arXiv.
Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger, 12th International Conference on Reversible Computation, 2020. [pdf] [arXiv]
Peng Fu, Peter Selinger, 2018. [arXiv]
Peng Fu, 2017. [arXiv]
Peng Fu, 2017. [arXiv]
Aaron Stump, Peng Fu. Journal of Functional Programming, 2016. [pdf]
Peng Fu, Ekaterina Komendantskaya, Tom Schrijvers, Andrew Pond. International Symposium on Functional and Logic Programming, 2016. [pdf]
Peng Fu, Ekaterina Komendantskaya. Formal Aspect of Computing, 2016 [pdf]
Peng Fu, Ekaterina Komendantskaya. International Symposium on Logic-Based Program Synthesis and Transformation, 2015. [pdf]
Peng Fu, Dissertation, 2014. [pdf]
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]
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.
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.
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.
Proto-Quipper: a quantum programming language, July 2nd, 2021, Logic, Quantum Computing, and Artificial Intelligence, Online workshop.
Linear dependent theory for quantum programming languages, June 11th, 2021, QPL, Online conference.
Fun with cryptography, Feb 24th, 2021, Math Circles monthly online event, Dalhousie University. [slides]
Linear dependent theory for quantum programming languages, July 8th, 2020, LICS, Online conference. [talk]
Linear dependent types for quantum circuit programming, February 17th, 2020, PL Reading Group, University of Maryland, College Park, Maryland, USA. [Slides]
Dependent types in Proto-quipper, September 20th, 2018, Dagstuhl Seminar: Quantum Programming Languages, Dagstuhl, Germany.
Encoding Data in Lambda Calculus: An Introduction, September 26th, 2017, Atlantic Category Seminar, Dalhousie University, Canada. [Slides]
Proof Relevant Corecursive Resolution, June 22nd, 2016, The Scottish Programming Languages Seminar, Heriot-Watt University, Edinburgh, UK. [Slides]
A Type-Theoretic Approach to Structural Resolution, July 13th, 2015, LOPSTR, Siena, Italy. [Slides]
Self Types for Dependently Typed Lambda Encodings, July 15th, 2014, RTA-TLCA, Vienna, Austria. [Slides]
Lambda Encodings in Type Theory, May 2nd, 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, May 2013. [pdf]
Remarks: This is my comprehensive exam paper.
Dependently-typed Programming with Scott Encoding. Peng Fu, Aaron Stump. 2013. [pdf]
Lambda Encoding with Comprehension, October 2013. [pdf]
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 note shows examples of realization by termination and realization by shape index.