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多态类型系统中的观察：通过对量子态进行柯里化，可直接在复杂电路内部应用量子门。通过引入离散化透镜概念来控制这一柯里化过程，我们得以将电路结构的组合特性与量子门的计算内容分离开来。基于此方法，我们自底向上递归地定义了量子电路，并以组合方式证明了其正确性。