My research interests are in type theories, quantum programming languages and their categorical semantics. I am teaching CSCE 790:008 Quantum Programming Languages in Spring 2025. I am currently looking for one or two Ph.D. students, please see here for more information.
Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger. [pdf] [arXiv]
Peng Fu, Peter Selinger, 29th Workshop on Logic, Language, Information and Computation (WOLLIC 2023). [pdf] [arXiv]
Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger, 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023). [pdf] [arXiv]
Peng Fu, Kohei Kishida, Peter Selinger, Logical Methods in Computer Science, September 7, 2022, Volume 18, Issue 3. [pdf] [arXiv]
Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger, manuscript, 2022. [pdf] [arXiv]
Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger, to appear in 19th International Conference on Quantum Physics and Logic (QPL), 2022. [pdf] [arXiv]
Peng Fu, Kohei Kishida, Peter Selinger, 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020. [pdf] [talk]
Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger, 12th International Conference on Reversible Computation, 2020. [pdf] [arXiv]
Peng Fu, manuscript, 2017. [arXiv]
Peng Fu, manuscript, 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]
Proto-Quipper with Reverse and Control, Annual Quantum Symposium, June 13-14, 2024, Raleigh, NC, USA. [video]
Proto-Quipper with Reverse and Control, Quantum Circuit Design Automation, June 2-7, 2024, Kelowna, BC, Canada. [video]
Poster: Programming Quantum Circuits in Proto-Quipper, Nov 18-19, 2023, NC State Quantum Workshop, NC State University, Raleigh, NC, USA. [poster]
Introduction to Compact Closed Categories (and Dagger Categories), Nov 17, 2023, Quantum Information and Analysis Seminars at the University of South Carolina. [abstract]
An introduction to compact closed categories, Nov 10, 2023, Quantum Information and Analysis Seminars at the University of South Carolina. [abstract]
Proto-Quipper with Dynamic Lifting, Oct 23, 2023, invited talk, Center for Quantum and Topological Systems (CQTS) at New York University Abu Dhabi, Online. [slides]
Designing Quantum Programming Languages with Types, Oct 6, 2023, invited talk, Seminar in Advances in Computing, Computer Science and Engineering Department, Columbia, SC, USA. [slides]
Quantum computing: a brief introduction and some research topics, Sep 25, Oct 2, 2023, invited talk, the Artificial Intelligence Institute of University of South Carolina, Columbia, SC, USA. [slides]
Towards an induction principle for nested data types, July 13, 2023, 29th Workshop on Logic, Language, Information and Computation, WoLLIC 2023, Halifax, Canada. [slides]
Towards an induction principle for nested data types, June 8, 2023, 30th Foundational Methods in Computer Science Workshop, Mount Allison University, Sackville, New Brunswick, Canada.
Designing quantum programming languages with types, April 26, 2023, University of South Carolina, Online.
Proto-Quipper with dynamic lifting, April 5, 2023, Quantum Information Theory seminar, University of Bristol. Online.
Designing quantum programming languages with types, March 17, 2023, Toronto Metropolitan University, Toronto, Canada.
Proto-Quipper with dynamic lifting, January 20, 2023, 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023, online talk). [slides]
Proto-Quipper with dynamic lifting, June 27th - July 1st, 2022, 19th International Conference on Quantum Physics and Logic, Oxford, UK. [slides]
A biset-enriched categorical model for Proto-Quipper with dynamic lifting, June 27th - July 1st, 2022, 19th International Conference on Quantum Physics and Logic, Oxford, UK. [slides]
A biset-enriched categorical model for Proto-Quipper with dynamic lifting, June 21st - June 26th, 2022, 29th Foundational Methods in Computer Science Workshop (FMCS), University of Calgary, Canada. [slides]
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, 18th International Conference on Quantum Physics and Logic, 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, 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Online conference. [talk]
A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper, July 10th, 2020, 12th Conference on Reversible Computation, Online conference.
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, 25th International Symposium on Logic-Based Program Synthesis and Transformation, Siena, Italy. [slides]
Self Types for Dependently Typed Lambda Encodings, July 15th, 2014, Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications, 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, Workshop on Dependently-Typed Programming, Boston, MA. [slides]
A Framework for Internalizing Relations into Type Theory, August 2011, International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Wroclaw. Poland. [slides]