Il lambda-calcolo tipato e la corrispondenza Curry-Howard. Sistema T. Sistema F e aritmetica funzionale del secondo ordine. Logica Lineare.
[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