A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper

Abstract

We introduce dependently typed Proto-Quipper, or Proto-Quipper-D for short, an experimental quantum circuit programming language with linear dependent types. We give several examples to illustrate how linear dependent types can help in the construction of correct quantum circuits. Specifically, we show how dependent types enable programming families of circuits, and how dependent types solve the problem of type-safe uncomputation of garbage qubits. We also discuss other language features along the way.

Added a section on related work and a paragraph explaining qubit initialization and termination

References in corpus (4)

• Supplementary information for "Quantum supremacy using a programmable superconducting processor"
• Programmable Quantum Simulations of Spin Systems with Trapped Ions
• Exponential algorithmic speedup by quantum walk
• Linear Dependent Type Theory for Quantum Programming Languages

Cited by in corpus (6)

• Integration of Quantum Accelerators with High Performance Computing -- A Review of Quantum Programming Tools
• Linear Dependent Type Theory for Quantum Programming Languages
• A Biset-Enriched Categorical Model for Proto-Quipper with Dynamic Lifting
• Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
• Proto-Quipper with Reversing and Control
• Encoding High-level Quantum Programs as SZX-diagrams