El cálculo-lambda: de tipos simples a tipos con intersección no idempotente

Breve resumen de la materia

En este curso estudiaremos dos versiones tipadas del cálculo lambda. La primera es el cálculo lambda simplemente tipado, que es el equivalente computacional, a través de la
correspondencia Curry-Howard, de la deducción natural para la lógica proposicional intuicionista. La segunda variante es la variante dotada de un sistema de tipos de
intersección no idempotente. Los tipos de intersección no idempotentes constituyen una herramienta poderosa para razonar sobre propiedades semánticas cualitativas y
cuantitativas de los programas: no sólo caracterizan diferentes nociones de terminación, sino que cualquier derivación de tipos da una cota para el tiempo de ejecución de un
programa.

Objetivos del curso
El objetivo del curso es presentar los sistemas de tipos con intersección no idempotente para el cálculo lambda. Esta línea de investigación fue iniciada por Philippa Gardner en los años 90 y recientemente ha recibido un gran interés en la comunidad de semántica de lenguajes de programación y lógica para ciencias de la computación. El curso cubre algunos resultados recientes en la literatura, mostrando la flexibilidad de este sistema de tipos para extraer información cualitativa y cuantitativa sobre programas y ejecuciones.
El curso también puede verse como una introducción suave a (algunos aspectos de) la teoría y semántica de los lenguajes de programación. Se propone un enfoque que combina
ejemplos y ejercicios para dar a los estudiantes intuiciones, con pruebas rigurosas de las propiedades más importantes, que dan a los estudiantes una idea de lo que significa trabajar con métodos formales, lógicos y matemáticos en las ciencias de la computación.

Programa
1. Deducción natural intuicionista proposicional, correspondencia de Curry-Howard, cálculo lambda simplemente tipado.
2. Cálculo lambda no tipado. Conceptos de reducción. Normalización débil y fuerte.
3. Tipos de intersección no idempotentes. Lema de sustitución, reducción y expansión del sujeto.
4. Resultados cualitativos: caracterización de la normalización de la reducción a la cabeza, normalización débil, normalización fuerte.
5. Resultados cuantitativos: cómo extraer límites superiores y exactos a la longitud de la evaluación mediante derivaciones de tipo.
6. Tipos de intersección no idempotentes para el cálculo lambda de débil en su variante call-by-value.
7. El problema de habitabilidad para los tipos de intersección no idempotentes.

Prerrequisitos

Nociones básicas de álgebra. Familiaridad con la lógica proposicional.
Opcional: conocimientos de lógica e inducción.

Bibliografía
– Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner. Tight typings and split bounds, fully developed. Journal of Functional Programming, vol. 30, e14, 2020.
– Beniamino Accattoli, Giulio Guerrieri. The Theory of Call-by-Value Solvability. Proceedings of the ACM on Programming Languages, vol. 6, issue ICFP (27th International Conference on Functional Programming, 2022), pp. 855–885, ACM, 2022.
– Victor Arrial, Giulio Guerrieri, Delia Kesner. Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework, to appear in the Proceedings of the ACM on Programming Languages, vol. 7, issue POPL (50th ACM SIGPLAN Symposium on Principles of Programming Languages, 2023), ACM, 2023.
– Henk P. Barendregt. The Lambda-Calculus. Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol. 103, North Holland, 1984.
– Antonio Bucciarelli, Thomas Ehrhard, Giulio Manzonetto. Not enough points is enough. Proceedings of the 16th annual conference Computer Science and Logic (CSL 2007),
LNCS, vol. 4646, pp. 268–282, 2007.
– Antonio Bucciarelli, Thomas Ehrhard, Giulio Manzonetto. A relational semantics for parallelism and non-determinism in a functional setting. Annals of Pure and Applied Logic, vol. 163, issue 7, pp. 918–934, 2012.
– Antonio Bucciarelli, Delia Kesner, Simona Ronchi Della Rocca. Inhabitation for Nonidempotent Intersection Types. Logical Methods in Computer Science, vol. 14, issue 3, 2018.
– Antonio Bucciarelli, Delia Kesner, Daniel Ventura. Non-Idempotent Intersection types for the Lambda-Calculus. Logic Journal of the IGPL, vol. 25, issue 4, pp. 431–464, 2017.
– Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Mathematical Structures in Computer Science, vol. 28, issue 7, pp. 1169-1203, 2018.
– Philippa Gardner. Discovering Needed Reductions Using Type Theory. Theoretical Aspects of Computer Software, International Conference (TACS 1994), LNCS, vol. 789, pp. 555–574,
1994. Student’s Preferred Background: The course only assumes very basic knowledge about discrete
– Jean-Yves Girard, Yves Lafont, Paul Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science, series number 7, Cambridge University Press, 1989.
– Giulio Guerrieri. Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus. Proceedings Twelfth Workshop on Developments in Computational
Models and Ninth Workshop on Intersection Types and Related Systems (DCM/ITRS 2018), EPTCS, vol. 293, pp. 57-72, 2019.