Publications

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 …
Cite DOI URL
Synthesizing Quantum-Circuit Optimizers
Near-term quantum computers are expected to work in an environment where each operation is noisy, with no error correction. Therefore, …
Cite DOI
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 …
Cite DOI
Modular Component-Based Quantum Circuit Synthesis
In this article, we present a novel method for synthesizing quantum circuits from user-supplied components. Given input-output state …
Cite DOI URL
Qunity: A Unified Language for Quantum and Classical Computing
We introduce Qunity, a new quantum programming language designed to treat quantum computing as a natural generalization of classical …
Cite DOI arXiv URL
Proto-Quipper with Dynamic Lifting
Quipper is a functional programming language for quantum computing. Proto-Quipper is a family of languages aiming to provide a formal …
Cite DOI arXiv URL
CoqQ: Foundational Verification of Quantum Programs
CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum …
Cite DOI arXiv URL
Verified Compilation of Quantum Oracles
Quantum algorithms often apply classical operations, such as arithmetic or predicate checks, over a quantum superposition of classical …
Cite DOI arXiv URL
Tower: Data Structures in Quantum Superposition
Emerging quantum algorithms for problems such as element distinctness, subset sum, and closest pair demonstrate computational …
Cite DOI arXiv URL
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 …
Cite arXiv
Scheme Pearl: Quantum Continuations
We advance the thesis that the simulation of quantum circuits is fundamentally about the efficient management of a large (potentially …
PDF Cite
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 …
Cite DOI arXiv
Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model
In a recent paper, a realizability technique has been used to give a semantics of a quantum lambda calculus. Such a technique gives …
Cite DOI
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 …
Cite DOI arXiv URL
Linear Dependent Type Theory for Quantum Programming Languages
Modern quantum programming languages integrate quantum resources and classical control. They must, on the one hand, be linearly typed …
Cite DOI
Mitiq: A software package for error mitigation on noisy quantum computers
We introduce Mitiq, a Python package for error mitigation on noisy quantum computers. Error mitigation techniques can reduce the impact …
Cite DOI URL
Verification of Distributed Quantum Programs
Distributed quantum systems and especially the Quantum Internet have the ever-increasing potential to fully demonstrate the power of …
Cite DOI arXiv
QIRO: A Static Single Assignment-Based Quantum Program Representation for Optimization
We propose an IR for quantum computing that directly exposes quantum and classical data dependencies for the purpose of optimization. …
Cite DOI arXiv
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 …
Cite DOI
Quartz: Superoptimization of Quantum Circuits
Existing quantum compilers optimize quantum circuits by applying circuit transformations designed by experts. This approach requires …
PDF Cite DOI arXiv URL
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, …
Cite DOI arXiv
Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra
We investigate the algebraic reasoning of quantum programs inspired by the success of classical program analysis based on Kleene …
Cite DOI arXiv
Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs
A first-order logic with quantum variables is needed as an assertion language for specifying and reasoning about various properties …
Cite arXiv
On Incorrectness Logic for Quantum Programs
Bug-catching is important for developing quantum programs. Motivated by the incorrectness logic for classical programs, we propose an …
Cite DOI URL
Bugs in Quantum Computing Platforms: An Empirical Study
The interest in quantum computing is growing, and with it, the importance of software platforms to develop quantum programs. Ensuring …
Cite DOI
A Quick Overview on the Quantum Control Approach to the Lambda Calculus
In this short overview, we start with the basics of quantum computing, explaining the difference between the quantum and the classical …
Cite DOI
A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm
Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but these are only useful if …
Cite arXiv URL
A biset-enriched categorical model for Proto-Quipper with dynamic lifting
Quipper and Proto-Quipper are a family of quantum programming languages that, by their nature as circuit description languages, involve …
Cite arXiv
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 …
Cite DOI arXiv
On Dynamic Lifting and Effect Typing in Circuit Description Languages (Extended Version)
In the realm of quantum computing, circuit description languages represent a valid alternative to traditional QRAM-style languages. …
Cite arXiv
Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
Quantum programming languages enable developers to implement algorithms for quantum computers that promise computational breakthroughs …
Cite DOI arXiv URL
Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages
The Pi family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type …
Cite DOI URL
Semantics for Variational Quantum Programming
We consider a programming language that can manipulate both classical and quantum information. Our language is type-safe and designed …
Cite DOI arXiv
Quantum Information Effects
We study the two dual quantum information effects to manipulate the amount of information in quantum computation: hiding and …
Cite DOI URL
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 …
Cite DOI
Quingo: A Programming Framework for Heterogeneous Quantum-Classical Computing with NISQ Features
The increasing control complexity of Noisy Intermediate-Scale Quantum (NISQ) systems underlines the necessity of integrating quantum …
Cite DOI URL
Quantum Hoare Logic with Classical Variables
Hoare logic provides a syntax-oriented method to reason about program correctness and has been proven effective in the verification of …
Cite DOI arXiv
Quantum and classical registers
We present a generic theory of “registers” in imperative programs and instantiate it in the classical and quantum setting. …
Cite arXiv
QIR Specification
The QIR specification is an effort of the QIR Alliance. It defines how to represent quantum programs within the LLVM IR.
Cite URL
Qimaera: Type-safe (Variational) Quantum Programming in Idris
Variational Quantum Algorithms are hybrid classical-quantum algorithms where classical and quantum computation work in tandem to solve …
Cite arXiv URL
Concrete Categorical Model of a Quantum Circuit Description Language with Measurement
In this paper, we introduce dynamic lifting to a quantum circuit-description language, following the Proto-Quipper language approach. …
Cite DOI
A proof system for disjoint parallel quantum programs
In this paper, we define the operational and denotational semantics of a special class of parallel quantum programs, namely disjoint …
Cite DOI
Quantum and Classical Registers
A formalization of the theory of quantum and classical registers as developed by (Unruh, Quantum and Classical Registers). In a …
Cite URL
Formal Verification of Quantum Programs: Theory, Tools and Challenges
Over the past 27 years, quantum computing has seen a huge rise in interest from both academia and industry. At the current rate, …
Cite arXiv
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 …
Cite DOI arXiv
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 …
Cite DOI URL
Quantum CPOs
We introduce the monoidal closed category qCPO of quantum cpos, whose objects are “quantized” analogs of omega-complete …
Cite DOI
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 …
Cite DOI
Gottesman Types for Quantum Programs
The Heisenberg representation of quantum operators provides a powerful technique for reasoning about quantum circuits, albeit those …
Cite DOI URL
Formal Methods for Quantum Programs: A Survey
While recent progress in quantum hardware open the door for significant speedup in certain key areas (cryptography, biology, chemistry, …
Cite arXiv
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 …
Cite URL
Geometry of Interaction for ZX-Diagrams
ZX-Calculus is a versatile graphical language for quantum computation equipped with an equational theory. Getting inspiration from …
Cite DOI HAL
A New Connective in Natural Deduction, and Its Application to Quantum Computing
We investigate an unsuspected connection between non-harmonious logical connectives, such as Prior’s tonk, and quantum computing. …
Cite DOI arXiv
Quantum Relational Hoare Logic with Expectations
We present a variant of the quantum relational Hoare logic from (Unruh, POPL 2019) that allows us to use “expectations” in …
Cite DOI
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 …
Cite DOI arXiv
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 …
Cite DOI
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 …
Cite URL
Quantum Abstract Interpretation
In quantum computing, the basic unit of information is a qubit. Simulation of a general quantum program takes exponential time in the …
PDF Cite DOI
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 …
Cite DOI URL
Gleipnir: Toward Practical Error Analysis for Quantum Programs
Practical error analysis is essential for the design, optimization, and evaluation of Noisy Intermediate-Scale Quantum(NISQ) computing. …
Cite DOI
Extending C++ for Heterogeneous Quantum-Classical Computing
We present qcor—a language extension to C++ and compiler implementation that enables heterogeneous quantum-classical programming, …
Cite DOI arXiv
Quantum projective measurements and the CHSH inequality in Isabelle/HOL
We present a formalization in Isabelle/HOL of quantum projective measurements, a class of measurements involving orthogonal projectors …
Cite arXiv
Quantum projective measurements and the CHSH inequality
This work contains a formalization of quantum projective measurements, also known as von Neumann measurements, which are based on …
Cite URL
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 …
Cite DOI arXiv
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 …
Cite DOI
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 …
Cite DOI arXiv URL
ZX-calculus for the working quantum computer scientist
The ZX-calculus is a graphical language for reasoning about quantum computation that has recently seen an increased usage in a variety …
Cite arXiv
Quantum Programming Languages
Quantum programming languages are essential to translate ideas into instructions that can be executed by a quantum computer. Not only …
Cite DOI URL
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 …
Cite arXiv URL
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 …
Cite DOI
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 …
Cite DOI URL
t$|$ket$\rangle$: a retargetable compiler for NISQ devices
We present t$|$ket$\rangle$, a quantum software development platform produced by Cambridge Quantum Computing Ltd. The heart of …
Cite DOI arXiv URL
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 …
Cite DOI
Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information
This work is an effort to formalise some quantum algorithms and results in quantum information theory. Formal methods being critical …
Cite URL
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 …
Cite DOI
Q# Language Specification
Q# is part of Microsoft’s Quantum Development Kit and provides rich IDE support and tools for program visualization and analysis. …
Cite URL
Quantum Software Engineering: Landscapes and Horizons
Quantum software plays a critical role in exploiting the full potential of quantum computing systems. As a result, it has been drawing …
Cite arXiv
Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract
Modern quantum programming languages integrate quantum resources and classical control. They must, on the one hand, be linearly typed …
Cite DOI
An Open-Source, Industrial-Strength Optimizing Compiler for Quantum Programs
Quilc is an open-source, optimizing compiler for gate-based quantum programs written in Quil or QASM, two popular quantum programming …
Cite DOI URL
A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper
We introduce dependently typed Proto-Quipper, or Proto-Quipper-D for short, an experimental quantum circuit programming language with …
Cite DOI arXiv
staq -- A full-stack quantum processing toolkit
We describe staq, a full-stack quantum processing toolkit written in standard C++. staq is a quantum compiler toolkit, comprising of …
Cite DOI arXiv URL
Silq: A High-Level Quantum Language with Safe Uncomputation and Intuitive Semantics
Existing quantum languages force the programmer to work at a low level of abstraction leading to unintuitive and cluttered code. A …
PDF Cite DOI
Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory
Inductive datatypes in programming languages allow users to define useful data structures such as natural numbers, lists, trees, and …
Cite DOI
Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory
We describe categorical models of a circuit-based (quantum) functional programming language. We show that enriched categories play a …
Cite DOI
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 …
Cite URL
Two linearities for quantum computing in the lambda calculus
We propose a way to unify two approaches of non-cloning in quantum lambda-calculi: logical and algebraic linearities. The first …
Cite DOI arXiv
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 …
Cite DOI
Categories for Quantum Theory: An Introduction
Monoidal category theory serves as a powerful framework for describing logical aspects of quantum theory, giving an abstract language …
Cite DOI
Formal Verification vs. Quantum Uncertainty
Quantum programming is hard: Quantum programs are necessarily probabilistic and impossible to examine without disrupting the execution …
Cite DOI
Formal Verification of Quantum Algorithms Using Quantum Hoare Logic
We formalize the theory of quantum Hoare logic (QHL) [TOPLAS 33(6),19], an extension of Hoare logic for reasoning about quantum …
Cite DOI
Realizability in the Unitary Sphere
In this paper we present a semantics for a linear algebraic lambda-calculus based on realizability. This semantics characterizes a …
Cite DOI arXiv
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 …
Cite DOI arXiv
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. …
Cite DOI arXiv
Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic
We develop a linear logical framework within the Hybrid system and use it to reason about the type system of a quantum lambda calculus. …
Cite DOI arXiv
An Applied Quantum Hoare Logic
We derive a variant of quantum Hoare logic (QHL), called applied quantum Hoare logic (aQHL for short), by: 1. restricting QHL to a …
PDF Cite DOI
Sized Types for Low-Level Quantum Metaprogramming
One of the most fundamental aspects of quantum circuit design is the concept of families of circuits parametrized by an instance size. …
Cite DOI arXiv
Quantum Programming Made Easy
We present IQu, namely a quantum programming language that extends Reynold’s Idealized Algol, the paradigmatic core of Algol-like …
Cite DOI
A HoTT Quantum Equational Theory (Extended Version)
This paper presents an equational theory for the QRAM model of quantum computation, formulated as an embedded language inside of …
Cite arXiv
Quantum Programming Languages (Dagstuhl Seminar 18381)
This report documents the program and the outcomes of Dagstuhl Seminar 18381 “Quantum Programming Languages”, which brought …
Cite DOI URL
Quantum Hoare Logic
We formalize quantum Hoare logic [TOPLAS 33(6),19]. In particular, we specify the syntax and denotational semantics of a simple model …
Cite URL
QPCF: Higher-Order Languages and Quantum Circuits
qPCF is a paradigmatic quantum programming language that extends PCF with quantum circuits and a quantum co-processor. Quantum circuits …
Cite DOI arXiv
Overview and Comparison of Gate Level Quantum Software Platforms
Quantum computers are available to use over the cloud, but the recent explosion of quantum software platforms can be overwhelming for …
Cite DOI
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 …
Cite URL
Universal Properties in Quantum Theory
We argue that notions in quantum theory should have universal properties in the sense of category theory. We consider the completely …
Cite DOI
Towards Large-Scale Functional Verification of Universal Quantum Circuits
We introduce a framework for the formal specification and verification of quantum circuits based on the Feynman path integral. Our …
Cite DOI
ReQWIRE: Reasoning about Reversible Quantum Circuits
Common quantum algorithms make heavy use of ancillae: scratch qubits that are initialized at some state and later returned to that …
Cite DOI
Quantum Relational Hoare Logic
We present a logic for reasoning about pairs of interactive quantum programs – quantum relational Hoare logic (qRHL). This logic …
Cite DOI arXiv
QDB: From Quantum Algorithms Towards Correct Quantum Programs
With the advent of small-scale prototype quantum computers, researchers can now code and run quantum algorithms that were previously …
Cite DOI
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. …
Cite DOI URL
Formally Verified Quantum Programming
The field of quantum mechanics predates computer science by at least ten years, the time between the publication of the Schrodinger …
Cite URL
Automated Equivalence Checking of Concurrent Quantum Systems
The novel field of quantum computation and quantum information has gathered significant momentum in the last few years. It has the …
Cite DOI URL
Reasoning about Parallel Quantum Programs
We initiate the study of parallel quantum programming by defining the operational and denotational semantics of parallel quantum …
Cite arXiv
Linear/Non-Linear Types for Embedded Domain-Specific Languages
Domain-specific languages are often embedded inside of general-purpose host languages so that the embedded language can take advantage …
Cite URL
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 …
Cite DOI arXiv
Cirq
Cirq is a Python library for writing, manipulating, and optimizing quantum circuits and running them against quantum computers and …
Cite DOI URL
From Symmetric Pattern-Matching to Quantum Control
One perspective on quantum algorithms is that they are classical algorithms having access to a special kind of memory with exotic …
Cite DOI arXiv
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 …
Cite DOI
QWIRE Practice: Formal Verification of Quantum Circuits in Coq
We describe an embedding of the QWIRE quantum circuit language in the Coq proof assistant. This allows programmers to write quantum …
Cite DOI
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 …
Cite DOI arXiv
A Categorical Model for a Quantum Circuit Description Language (Extended Abstract)
Quipper is a practical programming language for describing families of quantum circuits. In this paper, we formalize a small, but …
Cite DOI
ProjectQ: An Open Source Software Framework for Quantum Computing
We introduce ProjectQ, an open source software effort for quantum computing. The first release features a compiler framework capable of …
Cite DOI
Phantom Types for Quantum Programs
We explore the design space of using dependent types to type check and verify quantum circuits. We weigh the trade-offs between the …
Cite URL
Algorithmic Analysis of Termination Problems for Quantum Programs
We introduce the notion of linear ranking super-martingale (LRSM) for quantum programs (with nondeterministic choices, namely angelic …
Cite DOI
Typing Quantum Superpositions and Measurement
We propose a way to unify two approaches of non-cloning in quantum lambda-calculi. The first approach is to forbid duplicating …
Cite DOI
A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls
In this paper we present two flavors of a quantum extension to the lambda calculus. The first one, 𝜆𝜌, follows the approach of …
Cite DOI
Programming languages and compiler design for realistic quantum hardware
Quantum computing sits at an important inflection point. For years, high-level algorithms for quantum computers have shown considerable …
Cite DOI
Open Quantum Assembly Language
This document describes a quantum assembly language (QASM) called OpenQASM that is used to implement experiments with low depth quantum …
Cite arXiv URL
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 …
Cite DOI
Qiskit: An Open-Source Framework for Quantum Computing
Qiskit is an open-source framework for working with noisy quantum computers at the level of pulses, circuits, and algorithms. …
Cite DOI URL
Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning
The unique features of the quantum world are explained in this book through the language of diagrams, setting out an innovative visual …
Cite DOI
Semantics of higher-order quantum computation via geometry of interaction
While much of the current study on quantum computation employs low-level formalisms such as quantum circuits, several high-level …
Cite DOI arXiv
The Geometry of Parallelism: Classical, Probabilistic, and Quantum Effects
We introduce a Geometry of Interaction model for higher-order quantum computation, and prove its adequacy for a fully fledged quantum …
Cite DOI arXiv
QWIRE: A Core Language for Quantum Circuits
This paper introduces QWIRE (“choir”), a language for defining quantum circuits and an interface for manipulating them …
PDF Cite DOI
Invariants of Quantum Programs: Characterisations and Generation
Program invariant is a fundamental notion widely used in program verification and analysis. The aim of this paper is twofold: (i) find …
PDF Cite DOI
A Practical Quantum Instruction Set Architecture
We introduce an abstract machine architecture for classical/quantum computations—including compilation—along with a quantum …
Cite arXiv URL
Verification Logics for Quantum Programs
We survey the landscape of Hoare logics for quantum programs. We review three papers: “Reasoning about imperative quantum …
Cite arXiv
Foundations of Quantum Programming
Foundations of Quantum Programming discusses how new programming methodologies and technologies developed for current computers can be …
Cite DOI
Quantum Alternation: Prospects and Problems
We propose a notion of quantum control in a quantum programming language which permits the superposition of finitely many quantum …
Cite DOI
Formalization of Quantum Protocols using Coq
Quantum Information Processing, which is an exciting area of research at the intersection of physics and computer science, has great …
Cite DOI
Analysis of Quantum Entanglement in Quantum Programs using Stabilizer Formalism
Quantum entanglement plays an important role in quantum computation and communication. It is necessary for many protocols and …
Cite DOI
Algebraic and Logical Methods in Quantum Computation
This thesis contains contributions to the theory of quantum computation. We first define a new method to efficiently approximate …
Cite arXiv
Programming the Quantum Future
The Quipper language offers a unified general-purpose programming framework for quantum computation.
Cite DOI
ScaffCC: Scalable Compilation and Analysis of Quantum Programs
We present ScaffCC, a scalable compilation and analysis framework based on LLVM (Lattner and Adve, 2004), which can be used for …
Cite DOI arXiv
Algebraic Effects, Linearity, and Quantum Programming Languages
We develop a new framework of algebraic theories with linear parameters, and use it to analyze the equational reasoning principles of …
PDF Cite DOI
The ZX-calculus is complete for stabilizer quantum mechanics
The ZX-calculus is a graphical calculus for reasoning about quantum systems and processes. It is known to be universal for pure state …
Cite DOI
Quantum Recursion and Second Quantisation
This paper introduces a new notion of quantum recursion of which the control flow of the computation is quantum rather than classical …
Cite arXiv
LIQ$Ui|\rangle$: A Software Design Architecture and Domain-Specific Language for Quantum Computing
Languages, compilers, and computer-aided design tools will be essential for scalable quantum computing, which promises an exponential …
Cite arXiv
Alternation in Quantum Programming: From Superposition of Data to Superposition of Programs
We extract a novel quantum programming paradigm - superposition of programs - from the design idea of a popular class of quantum …
Cite arXiv
Applying Quantitative Semantics to Higher-Order Quantum Computing
Finding a denotational semantics for higher order quantum computation is a long-standing problem in the semantics of quantum …
Cite DOI arXiv
Verification of Quantum Programs
This paper develops verification methodology for quantum programs, and the contribution of the paper is two-fold. - Sharir, Pnueli and …
Cite DOI
An Introduction to Quantum Programming in Quipper
Quipper is a recently developed programming language for expressing quantum computations. This paper gives a brief tutorial …
Cite DOI arXiv
Quipper: A Scalable Quantum Programming Language
The field of quantum algorithms is vibrant. Still, there is currently a lack of programming languages for describing quantum …
Cite DOI arXiv
Scaffold: Quantum Programming Language
Quantum computing is of significant research interest because of its potential to radically alter the performance and asymptotic …
Cite URL
Floyd--Hoare Logic for Quantum Programs
Floyd–Hoare logic is a foundation of axiomatic semantics of classical programs, and it provides effective proof techniques for …
Cite DOI
Interacting Quantum Observables: Categorical Algebra and Diagrammatics
This paper has two tightly intertwined aims: (i) to introduce an intuitive and universal graphical calculus for multi-qubit systems, …
Cite DOI
Measurements and Confluence in Quantum Lambda Calculi With Explicit Qubits
This paper demonstrates how to add a measurement operator to quantum λ-calculi. A proof of the consistency of the semantics is given …
Cite DOI arXiv
An Overview of QML With a Concrete Implementation in Haskell
This paper gives an introduction to and overview of the functional quantum programming language QML. The syntax of this language is …
Cite DOI arXiv
Quantum Computation and Quantum Information: 10th Anniversary Edition
One of the most cited books in physics of all time, Quantum Computation and Quantum Information remains the best textbook in this …
Cite DOI
Towards a Formally Verified Functional Quantum Programming Language
This thesis looks at the development of a framework for a functional quantum programming language. The framework is first developed in …
Cite URL
Physics, Topology, Logic and Computation: A Rosetta Stone
In physics, Feynman diagrams are used to reason about quantum processes. In the 1980s, it became clear that underlying these diagrams …
Cite DOI arXiv
The Quantum IO Monad
The quantum IO monad is a purely functional interface to quantum programming implemented as a Haskell library. At the same time it …
PDF Cite DOI
Semantic Techniques in Quantum Computation
The study of computational processes based on the laws of quantum mechanics has led to the discovery of new algorithms, cryptographic …
Cite DOI
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 …
Cite DOI
Quantum Lambda Calculus
We discuss the design of a typed lambda calculus for quantum computation. After a brief discussion of the role of higher-order …
PDF Cite DOI
Predicate Transformer Semantics of Quantum Programs
This chapter presents a systematic exposition of predicate transformer semantics for quantum programs. It is divided into two parts: …
PDF Cite DOI
Extended Measurement Calculus
Measurement-based quantum computation (MBQC) has emerged as a new approach to quantum computation where the notion of measurement is …
Cite DOI
Abstract Interpretation Techniques for Quantum Computation
In this chapter, we present applications of abstract interpretation techniques in quantum computing. Quantum computing is a now …
Cite DOI
The Arrow Calculus as a Quantum Programming Language
We express quantum computations (with measurements) using the arrow calculus extended with monadic constructions. This framework …
Cite DOI
Hoare Logic for Quantum Programs
Hoare logic is a foundation of axiomatic semantics of classical programs and it provides effective proof techniques for reasoning about …
Cite arXiv
Measurement-Based Quantum Computation
Quantum computation offers a promising new kind of information processing, where the non-classical features of quantum mechanics are …
Cite DOI arXiv
Categorical Quantum Mechanics
This invited chapter in the Handbook of Quantum Logic and Quantum Structures consists of two parts: 1. A substantially updated version …
Cite DOI arXiv
QMC: A Model Checker for Quantum Systems
The novel field of quantum computation and quantum information has been growing at a rapid rate; the study of quantum information in …
Cite DOI arXiv
The Measurement Calculus
Measurement-based quantum computation has emerged from the physics community as a new approach to quantum computation where the notion …
PDF Cite DOI
Quantum Programming Languages: An Introductory Overview
The present article gives an introductory overview of the novel field of quantum programming languages (QPLs) from a pragmatic …
Cite DOI
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 …
PDF Cite DOI
Quantum Programming Languages: Survey and Bibliography
The field of quantum programming languages is developing rapidly and there is a surprisingly large literature. Research in this area …
Cite DOI URL
Structuring quantum effects: superoperators as arrows
We show that the model of quantum computation based on density matrices and superoperators can be decomposed into a pure classical …
Cite DOI arXiv
Quantum Weakest Preconditions
We develop a notion of predicate transformer and, in particular, the weakest precondition, appropriate for quantum computation. We show …
PDF Cite DOI
A Lambda Calculus for Quantum Computation with Classical Control
In this paper we develop a functional programming language for quantum computers by extending the simply-typed lambda calculus with …
PDF Cite DOI
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 …
PDF Cite DOI
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 …
Cite DOI arXiv
Communicating Quantum Processes
We define a language CQP (Communicating Quantum Processes) for modelling systems which combine quantum and classical communication and …
PDF Cite DOI arXiv
Towards a Quantum Programming Language
We propose the design of a programming language for quantum computing. Traditionally, quantum algorithms are frequently expressed at …
PDF Cite DOI
Toward a Software Architecture for Quantum Computing Design Tools
Compilers and computer-aided design tools will be essential for quantum computing. We present a computer-aided design flow that …
PDF Cite
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 …
Cite DOI arXiv
A Brief Survey of Quantum Programming Languages
This article is a brief and subjective survey of quantum programming language research.
Cite DOI
Toward an Architecture for Quantum Programming
It is becoming increasingly clear that, if a useful device for quantum computation will ever be built, it will be embodied by a …
Cite DOI arXiv
Structured Quantum Programming
Describes QCL
PDF Cite
Conventions for Quantum Pseudocode
A few conventions for thinking about and writing quantum pseudocode are proposed. The conventions can be used for presenting any …
PDF Cite DOI