Quantum Computing

Beyond Separation: Toward a Specification Language for Modular Reasoning about Quantum Programs

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# as a Quantum Algorithmic Language

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 …

A Rich Type System for Quantum Programs

We show that Gottesman's [1998] semantics for Clifford circuits based on the Heisenberg representation can be treated as a type system that can efficiently characterize a common subset of quantum programs. Our applications include (i) certifying …

The Essence of Q#

Ongoing project with the aim to establish firm mathematical foundations for the Q# programming language.

Toward a Type-Theoretic Interpretation of Q#

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, …

Toward Formalizing the Q# Programming Language

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 …

Extending Gottesman Types Beyond the Clifford Group

We extend our previous work on Gottesman Types to cover circuits beyond Clifford Group and introduce the notion of linear combination types.

Quantum Hoare Type Theory

Toward a unified system for programming, specifying, and reasoning about quantum programs.

Quantum Hoare Type Theory

As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. Inspired by Hoare Type Theory in classical computing, we propose Quantum Hoare Type Theory (QHTT) in which …

Gottesman Types for Quantum Programs

The Heisenberg representation of quantum operators provides a powerful technique for reasoning about quantum circuits, albeit those restricted to the common (non-universal) Clifford set H, S and CNOT. The Gottesman-Knill theorem showed that we can …