A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper
Programming Languages
2023-07-04 v2 Quantum Physics
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.
Cite
@article{arxiv.2005.08396,
title = {A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper},
author = {Peng Fu and Kohei Kishida and Neil J. Ross and Peter Selinger},
journal= {arXiv preprint arXiv:2005.08396},
year = {2023}
}
Comments
Added a section on related work and a paragraph explaining qubit initialization and termination