quantum circuits

An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits

We introduce a new paradigm for analysing and finding bugs in quantum circuits. In our approach, the problem is given by a ‍triple P C Q and the question is whether, given a set P of quantum states on the input of a circuit C, the set of quantum …

QSSA: An SSA-Based IR for Quantum Computing

Quantum computing hardware has progressed rapidly. Simultaneously, there has been a proliferation of programming languages and program optimization tools for quantum computing. Existing quantum compilers use intermediate representations (IRs) where …

On a Categorically Sound Quantum Programming Language for Circuit Description

This thesis contains contributions to the mathematical foundations of quantum programming languages. The likely arrival of scalable quantum computers in the not so distant future has resulted in a flurry of activity in the development of quantum …

Unqomp: Synthesizing Uncomputation in Quantum Circuits

A key challenge when writing quantum programs is the need for uncomputation: temporary values produced during the computation must be reset to zero before they can be safely discarded. Unfortunately, most existing quantum languages require tedious …

An Automated Deductive Verification Framework for Circuit-Building Quantum Programs

While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. In this paper we propose Qbricks, …

Formal Methods in Quantum Circuit Design

The design and compilation of correct, efficient quantum circuits is integral to the future operation of quantum computers. This thesis makes contributions to the problems of optimizing and verifying quantum circuits, with an emphasis on the …

Classical Control and Quantum Circuits in Enriched Category Theory

We describe categorical models of a circuit-based (quantum) functional programming language. We show that enriched categories play a crucial role. Following earlier work on QWire by Paykin et al., we consider both a simple first-order linear language …

qPCF: A Language for Quantum Circuit Computations

We propose qPCF, a functional language able to define and manipulate quantum circuits in an easy and intuitive way. qPCF follows the tradition of "quantum data & classical control" languages, inspired to the QRAM model. Ideally, qPCF computes finite …

QWIRE: A Core Language for Quantum Circuits

This paper introduces QWIRE ("choir"), a language for defining quantum circuits and an interface for manipulating them inside of an arbitrary classical host language. QWIRE is minimal---it contains only a few primitives---and sound with respect to …

Reasoning about General Quantum Programs over Mixed States

In this work we present a functional programming language for quantum computation over mixed states. More interestingly, we develop a set of equations for the resulting programming language, proposing the first framework for equational reasoning …