• Programa

    • Lambda cálculo tipado, propiedades, variantes, expresividad, normalización débil y fuerte. 
    • Deducción natural (DN) para lógica intuicionista y clásica, normalización de pruebas.
    • Cálculo de secuentes (CS), eliminación de corte, Relación entre DN y CS, absorción de reglas estructurales.
    • Interpretación computacional de lógica intuicionista, isomorfismo de Curry-De Bruijn-Howard. LJT de Herbelin. Eliminación de corte como pattern-matching.  
    • Estrategias de evaluación Call-by-Value y Call-by-Name. Continuation passing style. Operadores de control: computando con continuaciones.
    • Interpretación computacional de lógica clásica. No determismo de eliminación de corte. Double-negation translations y la relación con transformación CPS. Lógica clásica proposicional como sistema de tipos para lambda cálculo con operadores de control. 
    • Lógica linear, proof-nets, isomorfismo de CdBH para lógica linear.