Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model

Alejandro Díaz-Caro, Octavio Malherbe

In a recent paper, a realizability technique has been used to give a semantics of a quantum lambda calculus. Such a technique gives rise to an infinite number of valid typing rules…