Volver
Academic · Theory · Research
Lambda Calculus
HaskellLambda Calculus
Apuntes completos y dos trabajos prácticos sobre cálculo lambda desarrollados en el master de investigación de Paris-Saclay.
About
El cálculo lambda es el fundamento teórico de la programación funcional y un pilar de la teoría de tipos y la semántica de lenguajes de programación. Este trabajo profundiza en sus bases formales.
Los dos trabajos prácticos implementan, por un lado, un intérprete de cálculo lambda capaz de reducir expresiones paso a paso, y por otro, una extensión con tipado simple (Simply Typed Lambda Calculus) con inferencia de tipos.
Los apuntes, elaborados durante el curso, incluyen demostraciones de las propiedades principales: confluencia (Church-Rosser), normalización fuerte y débil, y la correspondencia de Curry-Howard.
El repositorio incluye los apuntes en PDF, los dos trabajos con código fuente y las memorias técnicas.
Highlights
- Fundamentos del cálculo lambda sin tipos y con tipos
- Estrategias de reducción: call-by-value, call-by-name
- Trabajo 1: implementación de un intérprete lambda
- Trabajo 2: extensión con tipos simples (Simply Typed Lambda)
- Apuntes detallados con demostraciones formales
- Conexiones con lenguajes funcionales modernos (Haskell, ML)