### Research

My research interests are in type theories and their applications. I enjoy doing research on quantum programming languages and their categorical semantics. I am working on the design and implementation of a version of Proto-Quipper, see a tutorial here.
I am also organizing the ATCAT seminar this semester, here is the current schedule.

### Papers

• On the Lambek embedding and the category of product-preserving presheaves.

Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger, manuscript, 2022. [pdf] [arXiv]

• Proto-Quipper with dynamic lifting.

Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger, manuscript, 2022. [pdf] [arXiv]

• A biset-enriched categorical model for Proto-Quipper with dynamic lifting.

Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger, 19th International Conference on Quantum Physics and Logic (QPL), 2022. [pdf] [arXiv]

• 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. [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.

• 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. [pdf] [arXiv]

• Dependently typed folds for nested data types.

Peng Fu, Peter Selinger, manuscript, 2018. [arXiv]

• A Type Checking Algorithm for Higher-rank, Impredicative and Second-order Types.

Peng Fu, manuscript, 2017. [arXiv]

• Representing Nonterminating Rewriting with $\mathbf{F}^2_{\mu}$.

Peng Fu, manuscript, 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]

### Projects

• Dependently typed Proto-Quipper. [Project link] [Tutorial in arXiv]

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.

• Dependently typed folds for nested data types. [Project link] [Paper documention in arXiv]

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.

• A Type Checking Algorithm for Higher-rank, Impredicative and Second-order Types. [Project link] [Paper documention in arXiv]

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).

• Gottlob: a theorem prover for verifying Scott-encoded programs. [Project link] [Documention]

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.

### Teaching

• Logic in Computer Science, 2021 Winter, Dalhousie University.

• An online class teaching the interactive theorem prover agda.
• I was the teaching assistant, I helped develop homework and projects. See here for the course materials.

• Discrete Structures I, 2020 Summer, Dalhousie University.

• The class is taught completely online. Here is a copy of revised version of lecture note that I wrote.
• I am a co-instructor.

• Discrete Structures I, 2019 Summer, Dalhousie University.

• The class syllabus is available here.
• A lecture note is available here.

### Talks

• 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]

### Notes

• 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.