We propose a type-theoretic framework for describing and proving properties of quantum computations, in particular those presented as quantum circuits. Our proposal is based on an observation that, in the polymorphic type system of Coq, currying on quantum states allows us to apply quantum gates directly inside a complex circuit. By introducing a discrete notion of lens to control this currying, we are further able to separate the combinatorics of the circuit structure from the computational content of gates. We apply our development to define quantum circuits recursively from the bottom up, and prove their correctness compositionally.

翻译：我们提出了一种类型论框架，用于描述和证明量子计算（特别是以量子电路形式呈现的计算）的属性。该框架基于以下观察：在Coq的多态类型系统中，对量子态进行柯里化（currying）使我们能够直接在复杂电路内部应用量子门。通过引入透镜（lens）的离散概念来控制这种柯里化过程，我们进一步能够将电路结构的组合逻辑与门的计算内容分离开来。我们应用这一方法自底向上递归地定义量子电路，并以组合方式证明其正确性。