Título: On the Completeness of a Syntactically Linear Logic
Director: Alejandro Díaz-Caro
Jurados:
Pablo Barenbaum (Universidad de Buenos Aires)
Octavio Malherbe (Universidad de la República)
Benoît Valiron (Université Paris-Saclay)

Resumen:
El cálculo L-S, una extensión del lenguaje de pruebas de la lógica lineal relacionado con la computación cuántica, ha sido dotado de una semántica concreta en [DCM23]. En este artículo, demostramos resultados de completitud para esta semántica con respecto a la equivalencia computacional. Introducimos una semántica operacional para L-S y demostramos su isomorfismo con la semántica categórica bajo ciertas condiciones. Además, mostramos que la categoría se puede restringir a semimódulos finitamente generados, los cuales poseen mejores propiedades.