Lm2-logica Matematica 2, Tipi e Logica Lineare

Programma

Il lambda-calcolo tipato e la corrispondenza Curry-Howard. Sistema T. Sistema F e aritmetica funzionale del secondo ordine. Logica Lineare.

Materiale Didattico

[1] Dispense fornite dal docente[2] Barendregt ''The Lambda-calculus'' (La Sapienza, matematica), North Holland 1984[3] Girard J.-Y., ''Proof-theory and Logical complexity'', Bibliopolis 1987[4] Girard, Lafont, Taylor ''Proofs and Types'', Cambridge University Press 1990[5] Krivine ''Lambda-calculus: types and models'', Masson 1990