论文标题
量子电路编程的教程介绍在依赖类型的原始Quipper中
A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper
论文作者
论文摘要
我们引入了依赖类型的原始Quipper或Proto-Quipper-D，用于简称具有线性类型的实验量子电路编程语言。我们提供了几个示例，以说明线性依赖类型如何有助于构建正确的量子电路。具体而言，我们展示了依赖类型如何启用电路的编程家庭，以及依赖类型如何解决垃圾Qubits类型安全的问题的问题。在此过程中，我们还讨论了其他语言功能。
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.
