Defensa de Tesina LCC: Luciano Barletta

Título: Lenguaje cuántico de control clásico basado en circuitos, con lógica de Hoare

Resumen:
Tradicionalmente, los algoritmos cuánticos se describieron en términos del modelo de circuitos cuánticos o mediante máquinas de Turing cuánticas. Ambos enfoques, sin embargo, presentan limitaciones importantes: los circuitos cuánticos permiten describir el flujo de datos, pero no el flujo de control, mientras que las máquinas de Turing cuánticas ofrecen una visión demasiado general y alejada de las arquitecturas físicas actuales.

Peter Selinger, en su artículo Towards a Quantum Programming Language, introduce un lenguaje funcional con control clásico y datos cuánticos. Su propuesta se aparta de los lenguajes imperativos anteriores al evitar errores en tiempo de ejecución gracias a un sistema de tipos estático, y se basa en una semántica denotacional rica, donde los programas son interpretados como superoperadores. Su enfoque permite razonar sobre programas cuánticos, incluyendo bucles y procedimientos recursivos, algo ausente en circuitos. Posteriormente, el desarrollo de Selinger evoluciona hacia un lambda-cálculo tipado y luego hacia un lenguaje funcional embebido en Haskell llamado Quipper.

En este trabajo se propone un nuevo lenguaje de programación cuántica, funcional pero con estilo imperativo, en el sentido de que los programas se estructuran como secuencias de comandos. El diseño está inspirado en el lenguaje gráfico de circuitos cuánticos y permite describir tanto operadores unitarios como mediciones. Además se provee una implementación embebida en Haskell y una lógica de Hoare para razonar formalmente sobre programas.