Linear types enforce no-cloning and no-deleting theorems in functional quantum programming. However, in imperative quantum programming, they have not gained widespread adoption. This work aims to develop a quantum type system that combines ergonomic …
We present ongoing work on Guppy, a domain-specific language embedded in Python that allows users to write high-level hybrid quantum programs with complex control flow in Pythonic syntax, aiming to run them on actual quantum hardware.
We show that Gottesman's (1998) semantics for Clifford circuits based on the Heisenberg representation gives rise to a lightweight Hoare-like logic for efficiently characterizing a common subset of quantum programs. Our applications include (i) …
There has been a recent surge of interest in separation logics for quantum computation. Unlike Reynolds' initial attempts to formulate a separation logic for reasoning about _pointer manipulation_ using small, intuitive programs, the attempts in the …
Q# is a standalone domain-specific 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 …
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, …
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. We aim to …