Frank (Peng) Fu
Email:
Website:
Mailing Address:

pfu@cse.sc.edu
https://cse.sc.edu/~pfu
Computer Science and Engineering Department,
Storey Innovation Center, Rm 2200
550 Assembly Street,Columbia, SC 29201

Education• Ph.D. Department of Computer Science, University of Iowa, Iowa City, Iowa, USA. September 2009 –August 2014. Advisor: Aaron Stump. Thesis Title: Lambda encodings in type theory.
• B.Eng. School of Computer Science, Huazhong University of Science and Technology, Wuhan, Hubei,
China. September 2005 – June 2009.

Academic positions• Assistant Professor, University of South Carolina, Columbia, South Carolina, USA. 2023 August –present• Postdoctoral Researcher, Dalhousie University, Halifax, Nova Scotia, Canada. May 2017 – August 2023.
• Lecturer, Discrete Structures I, Dalhousie University, Canada. May – July, 2019 and 2020.
• Postdoctoral Researcher, Heriot-Watt University, Edinburgh, Scotland, UK. March – August 2016.
• Postdoctoral Researcher, University of Dundee, Dundee, Scotland, UK. October 2014 – February 2016.

Publications[1] Peng Fu and Peter Selinger. Towards an Induction Principle for Nested Data Types. InHelle Hvid Hansen, Andre Scedrov, and Ruy J.G.B. de Queiroz, editors, Logic, Language, Information,and Computation, pages 244–255, Cham, 2023. Springer Nature Switzerland. Also available fromarXiv:2306.10124[2] Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. Proto-Quipper with Dynamic Lifting.
Proc. ACM Program. Lang., 7(POPL), jan 2023. Also available from arXiv:2204.13041[3] Peng Fu, Kohei Kishida, and Peter Selinger. Linear Dependent Type Theory for Quantum
Programming Languages. Logical Methods in Computer Science, Volume 18, Issue 3, September
2022[4] Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. A biset-enriched categorical modelfor Proto-Quipper with dynamic lifting. To appear in Proceedings of the 19th International
Conference on Quantum Physics and Logic (QPL 2022), Oxford, 2022.. Available from arXiv:2204.
13039, April 2022
[5] Peng Fu, Kohei Kishida, and Peter Selinger. Linear dependent type theory for quantum programming languages. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS 2020, Saarbrücken, Germany, pages 440–453, 2020. Also available fromarXiv:2004.13472

1

[6] Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. A tutorial introduction to quantum
circuit programming in dependently typed Proto-Quipper. In Proceedings of the 12th International Conference on Reversible Computation, RC 2020, Oslo, Norway, volume 12227 of Lecture Notes
in Computer Science, pages 153–168. Springer, 2020. Also available from arXiv:2005.08396[7] Peng Fu and Ekaterina Komendantskaya. Operational semantics of resolution and productivity
in Horn clause logic. Formal Aspects of Computing, 29(3):453–474, May 2017[8] Aaron Stump and Peng Fu. Efficiency of lambda-encodings in total type theory. Journal ofFunctional Programming, 26:e3, 2016[9] Peng Fu, Ekaterina Komendantskaya, Tom Schrijvers, and Andrew Pond. Proof Relevant Corecursive Resolution. In Oleg Kiselyov and Andy King, editors, Functional and Logic Programming,
pages 126–143, Cham, 2016. Springer International Publishing[10] Peng Fu and Ekaterina Komendantskaya. A Type-Theoretic Approach to Resolution. In
Moreno Falaschi, editor, Logic-Based Program Synthesis and Transformation, pages 91–106, Cham,
2015. Springer International Publishing[11] Peng Fu and Aaron Stump. Self Types for Dependently Typed Lambda Encodings. In GillesDowek, editor, Rewriting and Typed Lambda Calculi, pages 224–239, Cham, 2014. Springer InternationalPublishing[12] Garrin Kimmell, Aaron Stump, Harley D. Eades, Peng Fu, Tim Sheard, Stephanie Weirich, ChrisCasinghino, Vilhelm Sjöberg, Nathan Collins, and Ki Yung Ahn. Equational Reasoning about
Programs with General Recursion and Call-by-Value Semantics. In Proceedings of the Sixth
Workshop on Programming Languages Meets Program Verification, PLPV ’12, page 15–26, New York,NY, USA, 2012. Association for Computing Machinery[13] Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu,Garrin Kimmell, Tim Sheard, Aaron Stump, and Stephanie Weirich. Irrelevance, HeterogeneousEquality, and Call-by-value Dependent Type Systems. In James Chapman and Paul Blain
Levy, editors, Proceedings Fourth Workshop on Mathematically Structured Functional Programming,
MSFP@ETAPS 2012, Tallinn, Estonia, 25 March 2012, volume 76 of EPTCS, pages 112–162, 2012[14] Peng Fu, Aaron Stump, and Jeffrey Vaughan. A Framework for Internalizing Relations into
Type Theory. In PSATTT’11: International Workshop on Proof-Search in Axiomatic Theories andType Theories, Wroclaw, Poland, August 2011. Germain Faure, Stéphane Lengrand, Assia Mahboubi

Presentations and invited talks• Proto-Quipper with Dynamic Lifting, October 23, 2023, Center for Quantum and TopologicalSystems (CQTS) at New York University Abu Dhabi, Online.
• Designing Quantum Programming Languages with Types, October 6, 2023, invited talk, Seminar in Advances in Computing, Computer Science and Engineering Department, University of South
Carolina Columbia, SC, USA.
• Quantum computing: a brief introduction and some research topics, September 25, October
2, 2023, invited talk, the Artificial Intelligence Institute of University of South Carolina, Columbia,SC, USA.
• Towards an induction principle for nested data types, July 13, 2023, 29th Workshop on Logic,Language, Information and Computation, WoLLIC 2023, Halifax, Canada2

• 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 SouthCarolina, 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. Online.
• Programming quantum circuits with Proto-Quipper, Invited talk, Quantum Information Theory, December 4, 2022, CMS Winter Meeting, Toronto, Canada.
• Proto-Quipper with dynamic lifting, June 27th - July 1st, 2022, 19th International Conferenceon Quantum Physics and Logic, Oxford, UK.
• A biset-enriched categorical model for Proto-Quipper with dynamic lifting, June 27 - July
1, 2022, 19th International Conference on Quantum Physics and Logic, Oxford, UK.
• A biset-enriched categorical model for Proto-Quipper with dynamic lifting, 21 – 26 June,
2022, 29th Foundational Methods in Computer Science Workshop (FMCS), University of Calgary,Calgary, Canada.
• Proto-Quipper: a quantum programming language, July 2, 2021, Logic, Quantum Computing,and Artificial Intelligence, Online workshop.
• Linear dependent theory for quantum programming languages, June 11, 2021, 18th International Conference on Quantum Physics and Logic, Online conference.
• Linear dependent theory for quantum programming languages, July 8, 2020, 35th Annual
ACM/IEEE Symposium on Logic in Computer Science, Online conference.
• A tutorial introduction to quantum circuit programming in dependently typed ProtoQuipper, July 10th, 2020, 12th Conference on Reversible Computation, Online conference.
• Linear dependent types for quantum circuit programming, February 17th, 2020, University ofMaryland, College Park, Maryland, USA.
• Dependent types in Proto-Quipper, September 20, 2018, Dagstuhl Seminar: Quantum Programming Languages, Dagstuhl, Germany.
• Proof relevant corecursive resolution. June 22, 2016, The Scottish Programming Languages
Seminar, Heriot-Watt University, Edinburgh, UK.
• A type-theoretic approach to structural resolution. July 13, 2015, 25th International Symposium on Logic-Based Program Synthesis and Transformation, Siena, Italy.
• Self types for dependently typed lambda encodings. July 15, 2014, Joint 25th International
Conference on Rewriting Techniques and Applications and 12th International Conference on Typed
Lambda Calculi and Applications, Vienna, Austria.
• Dependent lambda encoding with self types. September 2013, ACM SIGPLAN Workshop onDependently-Typed Programming(DTP), Boston, MA.
• A framework for internalizing relations into type theory. August 2011, International Workshop
on Proof-Search in Axiomatic Theories and Type Theories, Wroclaw. Poland.
3Service• Organizer. Atlantic Category Theory Seminar (2022 Winter – 2023 Winter).
• Program committee member.
– The 8th International Conference on Formal Structures for Computation and Deduction (FSCD2023).
– The Third International Workshop on Programming Languages for Quantum Computing (PLanQC2022).
• Reviewer.
Conferences– The 20th International Conference on Quantum Physics and Logic (QPL 2023).
– The 19th International Conference on Quantum Physics and Logic (QPL 2022).
– The 9th International Conference on Foundations of Software Science and Computation Structures(FoSSaCS 2016).
– The 32nd International Conference on Logic Programming (ICLP 2016).
– The 24th International Conference on Rewriting Techniques and Applications (RTA 2013).
Journals– IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (2023).
– ACM Transactions on Quantum Computing (2023).
– Information and Computation (2023).
– Theoretical Computer Science (2022).
– Logical Methods in Computer Science (2021).
• Volunteering.
– Local organizer, 29th Workshop on Logic, Language, Information and Computation, WoLLIC
2023, Halifax, Canada, July 11–14, 2023.
– Local organizer, 15th International Conference on Quantum Physics and Logic, QPL 2018, Halifax,Canada, June 3–7, 2018.

Teaching• University of South Carolina– CSCE 330:002 Programming language structures. (Fall 2023)• Dalhousie University– Undergraduate courses∗ Discrete structures I (Summer 2019, Summer 2020).
– Course development∗ Topic in Logics: theorem proving in Agda, Spring 2021.
– Special lectures∗ Fun with cryptography, Math Circles monthly online event (February 2021, March 2022).
• University of Dundee (2015)4

– Introduction to functional programming in Haskell, Spring 2015.
• University of Iowa (2009 – 2014)– Graduate Teaching Assistant.

5