Algebraic lambda calculus as a base for a quantum logic

ALEJANDRO DÍAZ CARO

Ciudad Autónoma de Buenos Aires

Jornada; VII Jornadas de Fundamentos de Cuántica; 2018

The lambda calculus, introduced by Alonzo Church in the 30s, can be seen as the most basic model of computation, and can serve as a prototype of a programming language, but also as a key ingredient of a proof system for a formal logic. In the realm of quantum programming languages there are mainly two approaches: either classical-control (i.e. the quantum computer is seen as a black box to interact with, from a classical computer which send the tasks to perform) or quantum-control (i.e. the programming language can expose the quantum operations done in the quantum computer, such as a controlled gate). In this talk I will summarise several recent works on the algebraic lambda calculus in order to define a quantum lambda calculus with quantum control, using both, syntactic and semantics methods.