A lambda calculus for quantum computation

ALEJANDRO DÍAZ CARO

Brasilia

Workshop; XI Summer Workshop in Mathematics; 2019

Universidade de Brasília

There are two main approaches for quantum extensions to the lambda calculus. The first one and more developed, uses the so-called classical-control. The idea is to provide a classical description of quantum circuits: its wires, what operations to apply and to which qubits. The second one, uses the so-called quantum-control. The idea here is to provide a proper encoding of the quantum operations and linear combinations in order to understand its behaviour. In this talk, I will focus on the long road path for the second approach, starting from the linear-algebraic lambda calculus, and its vectorial type system, and the more recent lambdaS, which combines algebraic linearity with logical linearity. Finally, I will show some results of a work-in-progress to define a fully quantum lambda-calculus with quantum control using realizability techniques.In this talk I will do an overview of joint works with: Pablo Arrighi, Gilles Dowek, Benoit Valiron, Alexandre Miquel, Mauricio Guillermo, and Octavio Malherbe.