Muchos sistemas informáticos modernos son concurrentes: están compuestos de programas que se ejecutan simultáneamente y que se coordinan mediante el intercambio de mensajes. Establecer la correctitud de estos programas implica garantizar que se respetan los protocolos establecidos. Esta tarea es crucial, pero también compleja, y requiere técnicas de verificación capaces de analizar estructuras de comunicación sofisticadas.
Este curso aborda los fundamentos de dichas técnicas y enfatiza el uso de conceptos de la lógica para la verificación de programas, usando sistemas de tipos. Entre ellos destaca la correspondencia de Curry-Howard, una de las relaciones más profundas entre lógica y computación, la cual asegura que demostrar un teorema y escribir un programa correcto son, en esencia, la misma actividad vista desde perspectivas distintas.
Desde la perspectiva de Curry-Howard, la verificación de programas concurrentes se apoya en la Lógica Lineal de Girard para garantizar que los programas siempre respetan sus protocolos. Asumiendo conceptos básicos de lógica y programación, el curso presenta diferentes formulaciones de la Lógica Lineal que permiten el análisis estático de diversas estructuras de programación concurrente. El enfoque es gradual, acompañado de ejemplos y aplicaciones.
Objetivos del curso
Introducir los principios básicos de programación concurrente con paso de mensajes y las diferentes propiedades de correctitud que aplican en dicho ámbito.
Presentar técnicas de verificación estática para programas, en particular sistemas de tipos para concurrencia y sus propiedades asociadas.
Exponer los principios de la correspondencia de Curry-Howard en el caso concurrente, usando la Lógica Lineal como un mecanismo para obtener sistemas de tipos para procesos concurrentes.
Ilustrar los principios de verificación basados en Lógica Lineal en ejemplos prácticos y aplicaciones, considerando aspectos prácticos como comunicación asíncrona, tolerancia a fallos y protocolos multipartita.
El curso está orientado a estudiantes de máster y doctorado, y no asume requisitos específicos, solo familiaridad con conceptos básicos de lógica y programación.
Luís Caires, Frank Pfenning. Session Types as Intuitionistic Linear Propositions. In CONCUR, 2010.
Luís Caires, Frank Pfenning, Bernardo Toninho. Linear Logic Propositions as Session Types. In Mathematical Structures in Computer Science, 2016.
Dan Frumin, Emanuele D'Osualdo, Bas van den Heuvel, Jorge Pérez. A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency. In OOPSLA, 2022.
Simon J. Gay and Vasco T. Vasconcelos. Session Types. Cambridge University Press, 2025.
Jorge Pérez, Luís Caires, Frank Pfenning, Bernardo Toninho. Linear Logical Relations and Observational Equivalences for Session-Based Concurrency. In Information and Computation, 2014.
Un listado de referencias adicionales (incluyendo herramientas de verificación) será ofrecido al final del curso.
Desarrollado por el Departamento de Computación, FCEyN, UBA