and Statically Enforcing the No-Cloning Theorem
Q# is a high-level programming language from Microsoft for writing and running quantum programs. Like most industrial languages, it was designed without a formal specification, which can naturally lead to ambiguity in its interpretation. Further, currently, the Q# type system cannot statically prevent cloning of qubits. We aim to provide a formal specification and semantics for Q#, placing the language on a solid mathematical foundation, enabling further evolution of its design and type system (including enforcing no-cloning). This paper describes our current progress in designing λ-Q# (an idealized version of Q#), our solution to the qubit cloning problem in λ-Q#, and outlines the next steps.
Extended abstract accepted for a talk at PLanQC 2021 co-located with PLDI ‘21.
Errata: While comparing λ-Q# and Harper’s language MA with IQu and Reynold’s Idealized Algol, we wrote “but neither IA nor IQu maintains such separation” in our footnote on page 3, this is incorrect. Bob Harper points out in his commentary on PFPL:
… so-called monadic separation of commands from expressions was present from the very beginning …