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的多态类型系统中，量子态上的柯里化操作允许我们直接在复杂电路内部应用量子门。通过引入离散透镜概念来控制这种柯里化过程，我们进一步实现了电路结构组合逻辑与量子门计算内容的分离。基于此框架，我们自底向上递归定义量子电路，并组合式地证明其正确性。