Pedro Bonilla Nadal - Cálculo lambda y lógica intuicionista
El objetivo sería hacer una introducción del cálculo lambda como un lenguaje formal. Para ello:
- Introducimos notación de BNF
- Explicamos brevemente el cálculo no tipado
- Como solución de este problema el cálculo lambda tipado
- isomorfismo con lógica proposicional intuicionista
Formato de la propuesta
Indicar uno de estos:
- Charla corta (10 minutos)
- Charla (25 minutos)
Descripción
El objetivo sería hacer una introducción del cálculo lambda como un lenguaje formal. Para ello:
- Introducimos notación de BNF:
- Explicamos que es una sintaxis y una semántica formal
- Explicamos que es una forma rápida de dar sintaxis a lenguaje
- Explicamos brevemente el cálculo no tipado:
- Sintaxis (muy breve)
- Denotando las equivalencias beta y eta
- Hablamos de su problema con ZFC en el axioma de regularidad (posiblemente explicando también que es ZFC y porqué es importante)
- Como solución de este problema el cálculo lambda tipado
- Explicamos que se cambia, apoyados en que ya se conoce el no-tipado
-
Explicamos sobre el cálculo tipado del isomorfismo de Curry-Howard
- Web del proyecto:
Público objetivo
El objetivo de esta charla es generalista. Se espera que cualquier persona que sepa los fundamentos de la lógica pueda entenderla en su mayor parte. Aun así espero poder incluir detalles que hagan que merezca la pena a un público que ya conozca el formalismo, como la reflexión sobre ZFC.
Ponente(s)
Pedro Bonilla Nadal:
- Doble Graduado en Ingeniería informática y matemáticas
- Estudiante del Máster en Matemáticas de la Universidad Autónoma de Madrid
- Realizando un TFM justo sobre este tema, bajo la dirección de Ángel González Prieto
- Me interesan tanto la parte matemática de los problemas y estructuras derivadas de los diferentes formalismos de la computación, como la programación funcional en práctica: como se da en diferentes lenguajes, patrones de diseño asociados, etc.
Contacto(s)
- Nombre: Pedro Bonilla Nadal
- Email:
- Web personal:
- Mastodon (u otras redes sociales libres):
- Twitter:
- GitLab:
- Portfolio o GitHub (u otros sitios de código colaborativo): https://www.github.com/pedrobn23