Selected publications at LSV

We propose an extension of simply typed lambda-calculus to handle some properties of quantum computing. The equiprobable quantum superposition is taken as a commutative pair and the quantum measurement as a non-deterministic projection over it. Destructive interferences are achieved by introducing an inverse symbol with respect to pairs. The no-cloning property is ensured by using a combination of syntactic linearity with linear logic. Indeed, the syntactic linearity is enough for unitary gates, while a function measuring its argument needs to enforce that the argument is used only once.

   author = {D{\'i}az{-}Caro, Alejandro and Dowek, Gilles},
   institution = {Computing Research Repository},
   month = jan,
   note = {22~pages},
   number = {1601.04294},
   type = {Research Report},
   title = {Quantum superpositions and projective measurement in the lambda calculus},
   url = {},
   year = {2016},

About LSV

Select by Year