QWIRE

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

quantum algorithms:

**constructive mathematics**, **realizability**, **computability**

propositions as types, proofs as programs, computational trinitarianism

*QWIRE* (Paykin, Rand & Zdancewic 17) is a quantum programming language based on linear type theory combined with intuitionistic type theory via the exponential modality.

The original article

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

Using ambient homotopy type theory:

- Jennifer Paykin, Steve Zdancewic,
*A HoTT Quantum Equational Theory*, talk at QPL2019 (arXiv:1904.04371)

category: people