Quantum PL & Verification Bibliography
About
Papers
People
Venues
Tags
Posts
Variants
BibLaTeX
BibTeX
bibtex2html
BibBase
Mailing List
Light
Dark
Automatic
Publications
Type
Uncategorized
Conference paper
Journal article
Report
Book
Book section
Thesis
Software
Date
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
1996
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 …
Kartik Singhal
,
Kesha Hietala
,
Sarah Marshall
,
Robert Rand
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, …
Amanda Xu
,
Abtin Molavi
,
Lauren Pick
,
Swamit Tannu
,
Aws Albarghouthi
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 …
Yu-Fang Chen
,
Kai-Min Chung
,
Ondřej Lengál
,
Jyun-Ao Lin
,
Wei-Lun Tsai
,
Di-De Yen
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 …
Chan Gu Kang
,
Hakjoo Oh
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 …
Finn Voichick
,
Liyi Li
,
Robert Rand
,
Michael Hicks
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 …
Peng Fu
,
Kohei Kishida
,
Neil J. Ross
,
Peter Selinger
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 …
Li Zhou
,
Gilles Barthe
,
Pierre-Yves Strub
,
Junyi Liu
,
Mingsheng Ying
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 …
Liyi Li
,
Finn Voichick
,
Kesha Hietala
,
Yuxiang Peng
,
Xiaodi Wu
,
Michael Hicks
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 …
Charles Yuan
,
Michael Carbin
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 …
Thomas Häner
,
Vadym Kliuchnikov
,
Martin Roetteler
,
Mathias Soeken
,
Alexander Vaschillo
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 …
Vikraman Choudhury
,
Amr Sabry
,
Borislav Agapiev
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 …
Thien Nguyen
,
Alexander McCaskey
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 …
Alejandro Díaz-Caro
,
Octavio Malherbe
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 …
Andrew W. Cross
,
Ali Javadi-Abhari
,
Thomas Alexander
,
Niel de Beaudrap
,
Lev S. Bishop
,
Steven Heidel
,
Colm A. Ryan
,
Prasahnt Sivarajah
,
John Smolin
,
Jay M. Gambetta
,
Blake R. Johnson
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 …
Peng Fu
,
Kohei Kishida
,
Peter Selinger
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 …
Ryan LaRose
,
Andrea Mari
,
Sarah Kaiser
,
Peter J. Karalekas
,
Andre A. Alves
,
Piotr Czarnik
,
Mohamed El Mandouh
,
Max H. Gordon
,
Yousef Hindy
,
Aaron Robertson
,
Purva Thakre
,
Misty Wahl
,
Danny Samuel
,
Rahul Mistri
,
Maxime Tremblay
,
Nick Gardner
,
Nathaniel T. Stemen
,
Nathan Shammah
,
William J. Zeng
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 …
Yuan Feng
,
Sanjiang Li
,
Mingsheng Ying
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. …
David Ittah
,
Thomas Häner
,
Vadym Kliuchnikov
,
Torsten Hoefler
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 …
Kesha Hietala
Cite
DOI
Quartz: Superoptimization of Quantum Circuits
Existing quantum compilers optimize quantum circuits by applying circuit transformations designed by experts. This approach requires …
Mingkuan Xu
,
Zikun Li
,
Oded Padon
,
Sina Lin
,
Jessica Pointing
,
Auguste Hirth
,
Henry Ma
,
Jens Palsberg
,
Alex Aiken
,
Umut A. Acar
,
Zhihao Jia
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, …
Runzhou Tao
,
Yunong Shi
,
Jianan Yao
,
Xupeng Li
,
Ali Javadi-Abhari
,
Andrew W. Cross
,
Frederic T. Chong
,
Ronghui Gu
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 …
Yuxiang Peng
,
Mingsheng Ying
,
Xiaodi Wu
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 …
Mingsheng Ying
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 …
Peng Yan
,
Hanru Jiang
,
Nengkun Yu
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 …
Matteo Paltenghi
,
Michael Pradel
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 …
Alejandro Díaz-Caro
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 …
Yuxiang Peng
,
Kesha Hietala
,
Runzhou Tao
,
Liyi Li
,
Robert Rand
,
Michael Hicks
,
Xiaodi Wu
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 …
Peng Fu
,
Kohei Kishida
,
Neil J. Ross
,
Peter Selinger
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 …
Anurudh Peduri
,
Siddharth Bhat
,
Tobias Grosser
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. …
Andrea Colledan
,
Ugo Dal Lago
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 …
Charles Yuan
,
Christopher McNally
,
Michael Carbin
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 …
Vikraman Choudhury
,
Jacek Karwowski
,
Amr Sabry
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 …
Xiaodong Jia
,
Andre Kornell
,
Bert Lindenhovius
,
Michael Mislove
,
Vladimir Zamdzhiev
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 …
Chris Heunen
,
Robin Kaarsgaard
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 …
Xuan-Bach Le
,
Shang-Wei Lin
,
Jun Sun
,
David Sanan
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 …
{Quingo Development Team}
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 …
Yuan Feng
,
Mingsheng Ying
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. …
Dominique Unruh
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.
{QIR Alliance}
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 …
Liliane-Joy Dandy
,
Emmanuel Jeandel
,
Vladimir Zamdzhiev
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. …
Dongho Lee
,
Valentin Perrelle
,
Benoît Valiron
,
Zhaowei Xu
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 …
Mingsheng Ying
,
Li Zhou
,
Yangjia Li
,
Yuan Feng
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 …
Dominique Unruh
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, …
Marco Lewis
,
Sadegh Soudjani
,
Paolo Zuliani
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 …
Alexander McCaskey
,
Thien Nguyen
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 …
Kartik Singhal
,
John Reppy
Cite
DOI
URL
Quantum CPOs
We introduce the monoidal closed category qCPO of quantum cpos, whose objects are “quantized” analogs of omega-complete …
Andre Kornell
,
Bert Lindenhovius
,
Michael Mislove
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 …
Martin Kong
Cite
DOI
Gottesman Types for Quantum Programs
The Heisenberg representation of quantum operators provides a powerful technique for reasoning about quantum circuits, albeit those …
Robert Rand
,
Aarthi Sundaram
,
Kartik Singhal
,
Brad Lackey
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, …
Christophe Chareton
,
Sébastien Bardin
,
Dongho Lee
,
Benoît Valiron
,
Renaud Vilmart
,
Zhaowei Xu
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 …
Francisco Rios
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 …
Kostia Chardonnet
,
Benoît Valiron
,
Renaud Vilmart
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. …
Alejandro Díaz-Caro
,
Gilles Dowek
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 …
Yangjia Li
,
Dominique Unruh
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 …
Li Zhou
,
Gilles Barthe
,
Justin Hsu
,
Mingsheng Ying
,
Nengkun Yu
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 …
Anouk Paradis
,
Benjamin Bichsel
,
Samuel Steffen
,
Martin Vechev
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 …
Kartik Singhal
,
Sarah Marshall
,
Kesha Hietala
,
Robert Rand
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 …
Nengkun Yu
,
Jens Palsberg
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 …
Kesha Hietala
,
Robert Rand
,
Shih-Han Hung
,
Liyi Li
,
Michael Hicks
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. …
Runzhou Tao
,
Yunong Shi
,
Jianan Yao
,
John Hui
,
Frederic T. Chong
,
Ronghui Gu
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, …
Alexander McCaskey
,
Thien Nguyen
,
Anthony Santana
,
Daniel Claudino
,
Tyler Kharazi
,
Hal Finkel
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 …
Mnacho Echenim
,
Mehdi Mhalla
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 …
Mnacho Echenim
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 …
Christophe Chareton
,
Sébastien Bardin
,
François Bobot
,
Valentin Perrelle
,
Benoît Valiron
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 …
Mingsheng Ying
,
Yuan Feng
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 …
Kesha Hietala
,
Robert Rand
,
Shih-Han Hung
,
Xiaodi Wu
,
Michael Hicks
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 …
John van de Wetering
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 …
Bettina Heim
,
Mathias Soeken
,
Sarah Marshall
,
Christopher E. Granade
,
Martin Roetteler
,
Alan Geller
,
Matthias Troyer
,
Krysta M. Svore
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 …
Kartik Singhal
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 …
Bettina Heim
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 …
Anthony Bordg
,
Hanna Lachnitt
,
Yijun He
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 …
Seyon Sivarajah
,
Silas Dilkes
,
Alexander Cowtan
,
Will Simmons
,
Alec Edgington
,
Ross Duncan
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 …
Gushu Li
,
Li Zhou
,
Nengkun Yu
,
Yufei Ding
,
Mingsheng Ying
,
Yuan Xie
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 …
Anthony Bordg
,
Hanna Lachnitt
,
Yijun He
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 …
Giulia Meuli
,
Mathias Soeken
,
Martin Roetteler
,
Thomas Häner
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. …
{Microsoft}
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 …
Jianjun Zhao
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 …
Peng Fu
,
Kohei Kishida
,
Peter Selinger
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 …
Robert S. Smith
,
Eric C. Peterson
,
Mark G. Skilbeck
,
Erik J. Davis
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 …
Peng Fu
,
Kohei Kishida
,
Neil J. Ross
,
Peter Selinger
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 …
Matthew Amy
,
Vlad Gheorghiu
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 …
Benjamin Bichsel
,
Maximilian Baader
,
Timon Gehr
,
Martin Vechev
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 …
Romain Péchoux
,
Simon Perdrix
,
Mathys Rennela
,
Vladimir Zamdzhiev
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 …
Mathys Rennela
,
Sam Staton
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 …
Kartik Singhal
,
Robert Rand
,
Michael Hicks
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 …
Alejandro Díaz-Caro
,
Gilles Dowek
,
Juan Pablo Rinaldi
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 …
Margherita Zorzi
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 …
Chris Heunen
,
Jamie Vicary
Cite
DOI
Formal Verification vs. Quantum Uncertainty
Quantum programming is hard: Quantum programs are necessarily probabilistic and impossible to examine without disrupting the execution …
Robert Rand
,
Kesha Hietala
,
Michael Hicks
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 …
Junyi Liu
,
Bohua Zhan
,
Shuling Wang
,
Shenggang Ying
,
Tao Liu
,
Yangjia Li
,
Mingsheng Ying
,
Naijun Zhan
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 …
Alejandro Díaz-Caro
,
Mauricio Guillermo
,
Alexandre Miquel
,
Benoît Valiron
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 …
Dominique Unruh
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. …
Mathieu Huot
,
Sam Staton
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. …
Mohamed Yousri Mahmoud
,
Amy P. Felty
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 …
Li Zhou
,
Nengkun Yu
,
Mingsheng Ying
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. …
Matthew Amy
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 …
Luca Paolini
,
Luca Roversi
,
Margherita Zorzi
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 …
Jennifer Paykin
,
Steve Zdancewic
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 …
Michele Mosca
,
Martin Roetteler
,
Peter Selinger
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 …
Junyi Liu
,
Bohua Zhan
,
Shuling Wang
,
Shenggang Ying
,
Tao Liu
,
Yangjia Li
,
Mingsheng Ying
,
Naijun Zhan
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 …
Luca Paolini
,
Mauro Piccolo
,
Margherita Zorzi
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 …
Ryan LaRose
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 …
Matthew Amy
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 …
Mathieu Huot
,
Sam Staton
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 …
Matthew Amy
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 …
Robert Rand
,
Jennifer Paykin
,
Dongho Lee
,
Steve Zdancewic
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 …
Dominique Unruh
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 …
Yipeng Huang
,
Margaret Martonosi
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. …
Vlad Gheorghiu
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 …
Robert Rand
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 …
Ebrahim Ardeshir-Larijani
,
Simon J. Gay
,
Rajagopal Nagarajan
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 …
Mingsheng Ying
,
Li Zhou
,
Yangjia Li
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 …
Jennifer Paykin
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 …
Bert Lindenhovius
,
Michael Mislove
,
Vladimir Zamdzhiev
Cite
DOI
arXiv
Cirq
Cirq is a Python library for writing, manipulating, and optimizing quantum circuits and running them against quantum computers and …
{Cirq Developers}
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 …
Amr Sabry
,
Benoît Valiron
,
Juliana Kaizer Vizzotto
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 …
Mathys Rennela
,
Sam Staton
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 …
Robert Rand
,
Jennifer Paykin
,
Steve Zdancewic
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 …
Krysta M. Svore
,
Alan Geller
,
Matthias Troyer
,
John Azariah
,
Christopher E. Granade
,
Bettina Heim
,
Vadym Kliuchnikov
,
Mariia Mykhailova
,
Andres Paz
,
Martin Roetteler
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 …
Francisco Rios
,
Peter Selinger
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 …
Damian S. Steiger
,
Thomas Häner
,
Matthias Troyer
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 …
Robert Rand
,
Jennifer Paykin
,
Steve Zdancewic
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 …
Yangjia Li
,
Mingsheng Ying
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 …
Alejandro Díaz-Caro
,
Gilles Dowek
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 …
Alejandro Díaz-Caro
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 …
Frederic T. Chong
,
Diana Franklin
,
Margaret Martonosi
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 …
Andrew W. Cross
,
Lev S. Bishop
,
John A. Smolin
,
Jay M. Gambetta
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 …
Luca Paolini
,
Margherita Zorzi
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. …
{Qiskit Community}
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 …
Bob Coecke
,
Aleks Kissinger
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 …
Ichiro Hasuo
,
Naohiko Hoshino
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 …
Ugo Dal Lago
,
Claudia Faggian
,
Benoît Valiron
,
Akira Yoshimizu
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 …
Jennifer Paykin
,
Robert Rand
,
Steve Zdancewic
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 …
Mingsheng Ying
,
Shenggang Ying
,
Xiaodi Wu
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 …
Robert S. Smith
,
Michael J. Curtis
,
William J. Zeng
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 …
Robert Rand
Cite
arXiv
Foundations of Quantum Programming
Foundations of Quantum Programming discusses how new programming methodologies and technologies developed for current computers can be …
Mingsheng Ying
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 …
Costin Bădescu
,
Prakash Panangaden
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 …
Jaap Boender
,
Florian Kammüller
,
Rajagopal Nagarajan
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 …
Kentaro Honda
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 …
Neil J. Ross
Cite
arXiv
Programming the Quantum Future
The Quipper language offers a unified general-purpose programming framework for quantum computation.
Benoît Valiron
,
Neil J. Ross
,
Peter Selinger
,
D. Scott Alexander
,
Jonathan M. Smith
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 …
Ali Javadi-Abhari
,
Shruti Patil
,
Daniel Kudrow
,
Jeff Heckey
,
Alexey Lvov
,
Frederic T. Chong
,
Margaret Martonosi
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 …
Sam Staton
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 …
Miriam Backens
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 …
Mingsheng Ying
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 …
Dave Wecker
,
Krysta M. Svore
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 …
Mingsheng Ying
,
Nengkun Yu
,
Yuan Feng
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 …
Michele Pagani
,
Peter Selinger
,
Benoît Valiron
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 …
Mingsheng Ying
,
Nengkun Yu
,
Yuan Feng
,
Runyao Duan
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 …
Alexander S. Green
,
Peter LeFanu Lumsdaine
,
Neil J. Ross
,
Peter Selinger
,
Benoît Valiron
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 …
Alexander S. Green
,
Peter LeFanu Lumsdaine
,
Neil J. Ross
,
Peter Selinger
,
Benoît Valiron
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 …
Ali Javadi-Abhari
,
Arvin Faruque
,
Mohammad Javad Dousti
,
Lukas Svec
,
Oana Catu
,
Amlan Chakrabarti
,
Chen-Fu Chiang
,
Seth Vanderwilt
,
John Black
,
Frederic T. Chong
,
Margaret Martonosi
,
Martin Suchara
,
Ken Brown
,
Massoud Pedram
,
Todd Brun
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 …
Mingsheng Ying
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, …
Bob Coecke
,
Ross Duncan
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 …
Alejandro Díaz-Caro
,
Pablo Arrighi
,
Manuel Gadella
,
Jonathan Grattage
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 …
Jonathan Grattage
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 …
Michael A. Nielsen
,
Isaac L. Chuang
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 …
Alexander S. Green
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 …
John C. Baez
,
Mike Stay
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 …
Thorsten Altenkirch
,
Alexander S. Green
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 …
Simon J. Gay
,
Ian Mackie
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 …
Juliana Kaizer Vizzotto
,
Giovani Rubert Librelotto
,
Amr Sabry
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 …
Peter Selinger
,
Benoît Valiron
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: …
Mingsheng Ying
,
Runyao Duan
,
Yuan Feng
,
Zhengfeng Ji
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 …
Vincent Danos
,
Elham Kashefi
,
Prakash Panangaden
,
Simon Perdrix
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 …
Philippe Jorrand
,
Simon Perdrix
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 …
Juliana Kaizer Vizzotto
,
André Rauber Du Bois
,
Amr Sabry
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 …
Mingsheng Ying
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 …
Hans J. Briegel
,
Dan E. Browne
,
Wolfgang Dür
,
Robert Raußendorf
,
Maarten Van den Nest
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 …
Samson Abramsky
,
Bob Coecke
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 …
Simon J. Gay
,
Rajagopal Nagarajan
,
Nikolaos Papanikolaou
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 …
Vincent Danos
,
Elham Kashefi
,
Prakash Panangaden
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 …
Roland Rüdiger
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 …
Peter Selinger
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 …
Simon J. Gay
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 …
Juliana Kaizer Vizzotto
,
Thorsten Altenkirch
,
Amr Sabry
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 …
Ellie D'Hondt
,
Prakash Panangaden
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 …
Peter Selinger
,
Benoît Valiron
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 …
Krysta M. Svore
,
Alfred V. Aho
,
Andrew W. Cross
,
Isaac L. Chuang
,
Igor L. Markov
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 …
Thorsten Altenkirch
,
Jonathan Grattage
Cite
DOI
arXiv
Communicating Quantum Processes
We define a language CQP (Communicating Quantum Processes) for modelling systems which combine quantum and classical communication and …
Simon J. Gay
,
Rajagopal Nagarajan
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 …
Peter Selinger
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 …
Krysta M. Svore
,
Andrew W. Cross
,
Alfred V. Aho
,
Isaac L. Chuang
,
Igor L. Markov
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 …
Samson Abramsky
,
Bob Coecke
Cite
DOI
arXiv
A Brief Survey of Quantum Programming Languages
This article is a brief and subjective survey of quantum programming language research.
Peter Selinger
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 …
Stefano Bettelli
,
Tommaso Calarco
,
Luciano Serafini
Cite
DOI
arXiv
Structured Quantum Programming
Describes QCL
Bernhard Ömer
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 …
Emanuel Knill
PDF
Cite
DOI
Cite
×