Resumen

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

1. Introducir los principios básicos de programación concurrente con paso de mensajes y las diferentes propiedades de correctitud que aplican en dicho ámbito.
2. Presentar técnicas de verificación estática para programas, en particular sistemas de tipos para concurrencia y sus propiedades asociadas.
3. 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.
4. 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.

Idioma: Español

Listado de temas

El curso sigue una estructura basada en los siguientes cinco bloques, uno por clase, que abordarán los siguientes temas:

1. Introducción a los programas concurrentes, sistemas de tipos basados en sesiones, y a una lógica basada en recursos: la Lógica Lineal.
2. La interpretación de la Lógica Lineal como procesos concurrentes.
3. Una visión lógica de asincronía, tolerancia a fallos, y comunicación multipartita.
4. Recursos ilimitados y comunicación cliente-servidor.
5. Recursos ilimitados por medio de la lógica de implicaciones agrupadas (bunched implications).

Programa

Lunes — Introducción a los programas concurrentes y a la Lógica Lineal

La primera clase incluye una presentación general de la programación concurrente con paso de mensajes y las propiedades de correctitud más relevantes. Se exponen las nociones de protocolos y sistemas de tipos basados en sesiones (session types). Adicionalmente, esta clase presenta las nociones esenciales de la Lógica Lineal de Girard (el llamado fragmento multiplicativo).

Martes — La interpretación de la Lógica Lineal como procesos concurrentes

Esta clase propone la correspondencia de Curry-Howard en su forma más elemental, basada en el fragmento multiplicativo. Usando ejemplos, se ilustra cómo el resultado de la eliminación del corte en la Lógica Lineal coincide con la sincronización de procesos, una relación que garantiza estáticamente importantes propiedades de correctitud, en particular la ausencia de deadlocks.

Miércoles — Una visión lógica de aspectos prácticos

En esta clase se expone cómo la verificación basada en Lógica Lineal permite incorporar tres características prácticas de los sistemas concurrentes. La primera es la comunicación asíncrona, la cual permite mayor flexibilidad que la comunicación síncrona. La segunda es una extensión de la Lógica Lineal en donde los procesos y protocolos son tolerantes a fallos. Finalmente, se plantea un esquema para el análisis de procesos concurrentes que admite el uso de protocolos multipartita (entre tres o más participantes).

Jueves — Recursos ilimitados y comunicación cliente-servidor

Hasta aquí hemos analizado lógicas con recursos lineales, que deben usarse exactamente una vez. En esta clase se extiende la Lógica Lineal multiplicativa con la modalidad exponencial (‘!’, bang), la cual permite representar recursos que pueden usarse cero o muchas veces. Se expone la extensión correspondiente de la correspondencia de Curry-Howard, en la que ‘!’ se utiliza para verificar procesos cliente-servidor.

Viernes — Una visión alternativa a los recursos ilimitados

La última clase expone un avance reciente de investigación en el ámbito de la verificación de procesos concurrentes. Concretamente, se presenta una extensión de la Lógica Lineal multiplicativa, esta vez inspirada en la lógica de implicaciones agrupadas (bunched implications, BI) de O’Hearn y Pym. Esta variante nos permite analizar la noción de propiedad (ownership) en el contexto de procesos cliente-servidor.

Bibliografía sugerida

• 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.

Prerrequisitos

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.

Sobre el profesor

Jorge A. Pérez es profesor asociado en la Universidad de Groningen (Países Bajos), donde dirige el Grupo de Computación Fundamental, uno de los grupos de investigación del Instituto Bernoulli de Matemáticas, Informática e Inteligencia Artificial. El grupo está compuesto actualmente por cinco profesores, seis estudiantes de doctorado y un investigador postdoctoral.

Pérez obtuvo su doctorado en la Universidad de Bolonia (Italia) en 2010 y trabajó como investigador postdoctoral en la Universidad NOVA de Lisboa (Portugal) entre 2010 y 2014. Sus líneas de investigación se centran en la teoría de la concurrencia, la semántica de los lenguajes de programación y la lógica en informática. Ha dirigido cinco tesis doctorales y actualmente supervisa otras dos. Pérez ha publicado 25 artículos en revistas especializadas, 62 artículos en conferencias y workshops internacionales, y un capítulo de libro.

Entre 2019 y 2024, su investigación fue financiada por el Consejo Holandés de Investigación (NWO) mediante una prestigiosa beca personal (VIDI) titulada «Unifying Correctness for Communicating Software». Actualmente, Pérez dirige un consorcio nacional de investigación titulado «Cyclic Structures in Programs and Proofs», el cual agrupa cinco universidades Holandesas.

Desde junio de 2024, Pérez es miembro del consejo directivo del Instituto Bernoulli y jefe del departamento de Ciencias de la Computación, que comprende siete grupos de investigación y más de 30 investigadores.