Typed compositional quantum computation with lenses

Jacques Garrigue, Takafumi Saikawa

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…