Two linearities for quantum computing in the lambda calculus

ALEJANDRO DÍAZ CARO

Edimburgo

Workshop; Combining Viewpoints in Quantum Theory; 2018

The University of Edimburgh

I will discuss a recent joint work with Gilles Dowek [LNCS 10687:281-293, 2017] on lambda calculus with quantum control. We proposed a way to add a measurement operator to a lambda calculus with quantum control. In order to do so, we provided the calculus with a type system which is is linear on superposition, while allows cloning (canonical) base vectors. In addition, we provided an interpretation of the calculus where superposed types are interpreted as vector spaces and non-superposed types as their basis. Finally, I will give some clues on an ongoing work with Octavio Malherbe in which we are studying a categorical semantics for such a calculus.