Nivel 4

Curry–Howard

Proposiciones como tipos, pruebas como términos: el puente exacto entre la lógica y el cálculo lambda.

Adaptado de: Capítulo: Lógica proposicional (isomorfismo de Curry–Howard).

Contenido

1. El isomorfismo
2. Conectivos como construcciones
3. Normalización = evaluación