Robert Rand

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)

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