nLab Jennifer Paykin

• personal page

Selected writings

Introducing QWIRE, a quantum programming language based on linear type theory connected with intuitionistic type theory via the exponential modality:

• Jennifer Paykin, Robert Rand, Steve Zdancewic, QWIRE: a core language for quantum circuits, POPL 2017: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesJanuary 2017 Pages 846–858 (doi:10.1145/3009837.3009894)

Theoretical background:

• Jennifer Paykin, Linear/non-Linear Types For Embedded Domain-Specific Languages, 2018 (upenn:2752)

Application to verified programming after implementation in Coq:

• Robert Rand, Jennifer Paykin, Steve Zdancewic, QWIRE Practice: Formal Verification of Quantum Circuits in Coq, EPTCS 266, 2018, pp. 119-132 (arXiv:1803.00699)

• Robert Rand, Jennifer Paykin, Dong-Ho Lee, Steve Zdancewic, ReQWIRE: Reasoning about Reversible Quantum Circuits, EPTCS 287 (2019) 299-312 [arXiv:1901.10118, doi:10.4204/EPTCS.287.17]

Using ambient homotopy type theory:

• Jennifer Paykin, Steve Zdancewic, A HoTT Quantum Equational Theory, talk at QPL2019 [arXiv:1904.04371, pdf, pdf]

category: people