Título: Verificación estática de contratos para tipos de sesión en Haskell
Director: Hernán Melgratti
Jurados: Fernando Asteasuain, Carlos Gustavo Lopez Pombo.

Resumen:
El lenguaje de programación Haskell cuenta con diversas
implementaciones de tipos de sesiones binarias. En este trabajo estudiamos la
viabilidad de integrarlas con LiquidHaskell, una herramienta de verificación
estática que extiende el lenguaje con tipos refinados. Si bien la estructura
recursiva de las sesiones se puede codificar fácilmente mediante tipos
paramétricos, garantizar tanto la dualidad como el uso linear de los canales
requiere de extensiones del lenguaje de mayor complejidad. Nosotros partimos de
implementaciones existentes, y que utilizan distintas extensiones y mecanismos.
A partir de estas, en la medida en la que son compatibles con LiquidHaskell, 
exploramos la clase de contratos sobre la comunicación que se pueden escribir y
verificar. Para esto utilizamos dos técnicas: una simple de integrar, pero que
solo permite escribir contratos sobre cada mensaje, es decir, sin tener en
cuenta los valores anteriormente intercambiados; y que permite expresar
propiedades más ricas, incluyendo dependencias con los mensajes previos, pero
cuya integración es más compleja.