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