Alejandro Diaz-Caro
Universidad Nacional de Quilmes & Instituto de Ciencias de la Computación (CONICET/UBA)

En ciencias de la computación, es bien conocida la relación entre los lenguajes de programación, la lógica formal y la teoría de categorías en matemáticas. Esta relación se conoce como el isomorfismo de Curry-Howard-Lambek. La idea es que un programa bien tipado es la prueba de una fórmula lógica y es un morfismo en alguna categoría. Para diferentes lógicas, existen diferentes lenguajes de programación y diferentes categorías. Este isomorfismo es responsable de que podamos verificar formalmente la corrección de programas, diseñar lenguajes de programación con características avanzadas guiados por sus modelos y tener asistentes de pruebas matemáticas. En el caso de la computación cuántica, se han definido varios lenguajes de programación. Por un lado, están aquellos en el paradigma de "control clásico", que básicamente son una descripción de un circuito cuántico a alto nivel y permiten componer diferentes circuitos para formar programas más grandes. Por otro lado, están los lenguajes de "control cuántico", en los cuales se abstraen las operaciones cuánticas en primitivas del lenguaje y se consiguen lenguajes con características avanzadas, como permitir la superposición de flujos de control de programas o lenguajes para describir la superposición temporal que puede ocurrir, por ejemplo, en un tablero de óptica cuántica. En esta charla voy a explicar el isomorfismo de Curry-Howard-Lambek y los resultados recientes en el establecimiento de dicho isomorfismo para algunos lenguajes de programación con control cuántico.