Program Specifications

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 …

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 …

Quantum Hoare Type Theory: Extended Abstract

As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. In classical computing, formal verification and sound static type systems prevent several classes of bugs …