Toward a Type-Theoretic Interpretation of Q# and Statically Enforcing the No-Cloning Theorem

Abstract

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.