Introducing QWIRE, a quantum programming language based on linear type theory connected with intuitionistic type theory via the exponential modality:
Theoretical background:
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:
Last revised on November 13, 2023 at 17:39:43. See the history of this page for a list of all contributions to it.