Toward A Quantum Programming Language for Higher-Level Formal Verification. Finn Voichick and Michael Hicks. In Informal Proceedings of the Workshop on Programming Languages and Quantum Computing (PLanQC), June 2021.

We present QuantumOne, a quantum programming language formalized within the Coq proof assistant and designed for formal verification of quantum algorithms. This language allows for working with superpositions of tagged unions, allowing for quantum data more complicated than simple qubits. This paper outlines the formal syntax, operational semantics, and typing judgment of QuantumOne.

[ .pdf ]

@inproceedings{voichick21qone,
  title = {Toward A Quantum Programming Language for Higher-Level Formal Verification},
  booktitle = {Informal Proceedings of the Workshop on Programming Languages and Quantum Computing (PLanQC)},
  author = {Finn Voichick and Michael Hicks},
  year = 2021,
  month = jun
}

This file was generated by bibtex2html 1.99.