Compilación del lambda cálculo con matrices densidad en la máquina cuántica IBM-Q

Abstract

El cálculo λρ introducido por Díaz-Caro en 2017 es un lenguaje basado en el lambda cálculo con extensiones para la computación cuántica donde se utiliza un modelo de control clásico y datos cuánticos. Los estados cuánticos se describen mediante matrices de densidad, que permite operar con estados cuánticos mixtos. En esta tesina se provee un algoritmo para tipar λρ. Utilizando este algoritmo probamos que el tipado es NP-completo bajo condiciones de minimización de los tipos. Seguidamente analizamos la relación entre λρ y las aplicaciones actuales de la computación cuántica al definir una traducción de una versión modificada de λρ a Python y haciendo uso de la biblioteca de Qiskit. Además de probar su correctitud, implementamos estos algoritmos en el lenguaje funcional Haskell.