• Descargas

    Teóricas

    • Contenidos de la materia
    • Clase 1 - Lambda cálculo tipado
    • Clase 2 - Normalización fuerte. Tipos dependientes
    • Clase 3 - Deducción Natural. Lógica intuicionista.
    • Clase 4 - Normalisación en Deducción Natural
    • Clase 5 - Cálculo de secuentes
    • Clase 6 - Eliminación de corte para cálculo de secuentes
    • Clase 7 - Isomorfismo de C-deB-H para Lógica Intuicionista
    • Clase 8 - CBV, CBN, CPS
    • Clase 9 - Operadores de control
    • Clase 10 - Isomorfismo de C-deB-H para Lógica Clásica (1/2)
    • Clase 11 -  Isomorfismo de C-deB-H para Lógica Clásica (2/2)

      


    Prácticas

    • Práctica 1 - Lambda cálculo tipado
    • Práctica 2 - Deducción Natural y Lógica Intuicionista
    • Práctica 3 - Cálculo de Secuentes
    • Práctica 4 - Isomorfiso de C-deB-H para LI

     

    Parcial


    Ponencias de cierre (12/Jul/2012)

    • Problemas de Tipado en LOO - Nicolás Passerini
    • Introducción a Agda - Gabriela Steren
    • First-class prompts - Pablo Barenbaum
    • A Symmetric Lambda Calculus for Classical Program Extraction - Andrés Viso
    • The Pure Pattern Calculus - Carlos Lombardi


    Material de soporte

    • Guía de referencia rápida

     

    Otros links