quantum computing

QParallel: Explicit Parallelism for Programming Quantum Computers

We present a language extension for parallel quantum programming to (1) remove ambiguities concerning parallelism in current quantum programming languages and (2) facilitate space-time tradeoff investigations in quantum computing. While the focus of …

OpenQASM 3: A Broader and Deeper Quantum Assembly Language

Quantum assembly languages are machine-independent languages that traditionally describe quantum computation in the circuit model. Open quantum assembly language (OpenQASM 2) was proposed as an imperative programming language for quantum circuits …

Retargetable Optimizing Compilers for Quantum Accelerators via a Multilevel Intermediate Representation

We present a multilevel quantum-classical intermediate representation (IR) that enables an optimizing, retargetable compiler for available quantum languages. Our work builds upon the multilevel intermediate representation (MLIR) framework and …

A Verified Software Toolchain For Quantum Programming

Quantum computing is steadily moving from theory into practice, with small-scale quantum computers available for public use. Now quantum programmers are faced with a classical problem: How can they be sure that their code does what they intend it to …

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 …

Giallar: Push-Button Verification for the Qiskit Quantum Compiler

This paper presents Giallar, a fully-automated verification toolkit for quantum compilers. Giallar requires no manual specifications, invariants, or proofs, and can automatically verify that a compiler pass preserves the semantics of quantum …

Quartz: Superoptimization of Quantum Circuits

Existing quantum compilers optimize quantum circuits by applying circuit transformations designed by experts. This approach requires significant manual effort to design and implement circuit transformations for different quantum devices, which use …

A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic

It is well-known that quantum programs are not only complicated to design but also challenging to verify because the quantum states can have exponential size and require sophisticated mathematics to encode and manipulate. To tackle the state-space …

A MLIR Dialect for Quantum Assembly Languages

We demonstrate the utility of the Multi-Level Intermediate Representation (MLIR) for quantum computing. Specifically, we extend MLIR with a new quantum dialect that enables the expression and compilation of common quantum assembly languages. The true …

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 …

On the Impact of Affine Loop Transformations in Qubit Allocation

Most quantum compiler transformations and qubit allocation techniques to date are either peep-hole focused or rely on sliding windows that depend on a number of external parameters including the topology of the quantum processor. Thus, global …

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 …

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 …

A Quantum Interpretation of Bunched Logic & Quantum Separation Logic

We propose a model of the substructural logic of Bunched Implications (BI) that is suitable for reasoning about quantum states. In our model, the separating conjunction of BI describes separable quantum states. We develop a program logic where pre- …

Extending C++ for Heterogeneous Quantum-Classical Computing

We present qcor—a language extension to C++ and compiler implementation that enables heterogeneous quantum-classical programming, compilation, and execution in a single-source context. Our work provides a first-of-its-kind C++ compiler enabling …

Proving Quantum Programs Correct

As quantum computing progresses steadily from theory into practice, programmers will face a common problem: How can they be sure that their code does what they intend it to do? This paper presents encouraging results in the application of mechanized …

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

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

A Verified Optimizer for Quantum Circuits

We present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, a simple quantum intermediate representation, …

Model Checking Quantum Systems: Principles and Algorithms

Model checking is one of the most successful verification techniques and has been widely adopted in traditional computing and communication hardware and software industries. This book provides the first systematic introduction to model checking …

Certified Quantum Computation in Isabelle/HOL

In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. Formal methods being critical for the safety and security of algorithms and protocols, we …

Development of Quantum Applications

The aim of this thesis is to identify practical applications where quantum computing could have an advantage over what is achievable with conventional means of computing, and what advances are needed in order to actualize that potential. We …

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 …

Enabling Accuracy-Aware Quantum Compilers Using Symbolic Resource Estimation

Approximation errors must be taken into account when compiling quantum programs into a low-level gate set. We present a methodology that tracks such errors automatically and then optimizes accuracy parameters to guarantee a specified overall accuracy …

Projection-Based Runtime Assertions for Testing and Debugging Quantum Programs

In this paper, we propose Proq, a runtime assertion scheme for testing and debugging quantum programs on a quantum computer. The predicates in Proq are represented by projections (or equivalently, closed subspaces of the state space), following …

Verified translation between low-level quantum languages

We describe the ongoing development of a verified translator between OpenQASM (Open Quantum Assembly Language) and sqir, a Small Quantum Intermediate Representation used for circuit optimization. Verified translation from and to OpenQASM will allow …

Quantum Calculi---From Theory to Language Design

In the last 20 years, several approaches to quantum programming have been introduced. In this survey, we focus on the QRAM (Quantum Random Access Machine) architectural model. We explore the twofold perspective (theoretical and concrete) of the …

Formal Verification vs. Quantum Uncertainty

Quantum programming is hard: Quantum programs are necessarily probabilistic and impossible to examine without disrupting the execution of a program. In response to this challenge, we and a number of other researchers have written tools to verify …

Quantum channels as a categorical completion

We propose a categorical foundation for the connection between pure and mixed states in quantum information and quantum computation. The foundation is based on distributive monoidal categories. First, we prove that the category of all quantum …

Quantum Hoare Logic with Ghost Variables

Quantum Hoare logic allows us to reason about quantum programs. We present an extension of quantum Hoare logic that introduces "ghost variables" to extend the expressive power of pre-/postconditions. Ghost variables are variables that do not actually …

Quantum Programming Languages (Dagstuhl Seminar 18381)

This report documents the program and the outcomes of Dagstuhl Seminar 18381 "Quantum Programming Languages", which brought together researchers from quantum computing and classical programming languages.

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 …

Quantum++: A modern C++ quantum computing library

Quantum++ is a modern general-purpose multi-threaded quantum computing library written in C++11 and composed solely of header files. The library is not restricted to qubit systems or specific quantum information processing tasks, being capable of …

Enriching a Linear/Non-Linear Lambda Calculus: A Programming Language for String Diagrams

Linear/non-linear (LNL) models, as described by Benton, soundly model a LNL term calculus and LNL logic closely related to intuitionistic linear logic. Every such model induces a canonical enrichment that we show soundly models a LNL lambda calculus …

Q#: Enabling Scalable Quantum Computing and Development with a High-Level DSL

Quantum computing exploits quantum phenomena such as superposition and entanglement to realize a form of parallelism that is not available to traditional computing. It offers the potential of significant computational speed-ups in quantum chemistry, …

Open Quantum Assembly Language

This document describes a quantum assembly language (QASM) called OpenQASM that is used to implement experiments with low depth quantum circuits. OpenQASM represents universal physical circuits over the CNOT plus SU(2) basis with straight-line code …

Categorical Quantum Mechanics

This invited chapter in the Handbook of Quantum Logic and Quantum Structures consists of two parts: 1. A substantially updated version of quant-ph/0402130 by the same authors, which initiated the area of categorical quantum mechanics, but had not yet …

Dagger Compact Closed Categories and Completely Positive Maps (Extended Abstract)

Dagger compact closed categories were recently introduced by Abramsky and Coecke, under the name "strongly compact closed categories", as an axiomatic framework for quantum mechanics. We present a graphical language for dagger compact closed …

A Layered Software Architecture for Quantum Computing Design Tools

Compilers and computer-aided design tools are essential for fine-grained control of nanoscale quantum-mechanical systems. A proposed four-phase design flow assists with computations by transforming a quantum algorithm from a high-level language …

A Functional Quantum Programming Language

We introduce the language QML, a functional language for quantum computations on finite types. Its design is guided by its categorical semantics: QML programs are interpreted by morphisms in the category FQC of finite quantum computations, which …

Communicating Quantum Processes

We define a language CQP (Communicating Quantum Processes) for modelling systems which combine quantum and classical communication and computation. CQP combines the communication primitives of the pi-calculus with primitives for measurement and …

A Categorical Semantics of Quantum Protocols

We study quantum information and computation from a novel point of view. Our approach is based on recasting the standard axiomatic presentation of quantum mechanics, due to von Neumann, at a more abstract level, of compact closed categories with …