Quella che segue è una lista di domande che coprono tutti gli argomenti
visti a lezione. Per gli argomenti più complessi fornisco un puntatore a un
libro o articolo in cui è possibile trovare l'argomento trattato. Tutti gli
altri argomenti sono trattati in molteplici introduzione al lambda-calcolo.
Le note di Barendregt citate sotto o il "Proofs and Types" di Girard sono
buone referenze.

01. definizione di formalismo di calcolo
02. esempi di formalismi di calcolo
03. lambda-calcolo vs macchine di Turing: vantaggi e svantaggi
04. sintassi del lambda-calcolo: termini, precedenza, associatività
05. binders, variabili libere e legate
06. alpha-conversione e capture avoiding substitution
07. beta-riduzione
08. operatori di punto fisso nel lambda-calcolo
09. uso dell'operatore di punto fisso per implementare la ricorsione generale
10. esempio di termine divergente
11. tipi di dati algebrici
12. tipi di dati induttivi e co-induttivi (cenni)
13. encoding di Scott dei tipi di dati algebrici
    # "Programming in the λ-Calculus: From Church to Scott and Back",
      Jan Martin Jansen
14. Turing completezza del lambda-calcolo
15. sistemi di riscrittura astratti: definizione e prime proprietà
16. confluenza, semi-confluenza, confluenza debole e loro relazioni
17. unicità delle forme normali, safety e altre conseguenze della confluenza
18. dimostrazione del teorema di confluenza per il lambda-calcolo
    # "Introduction to lambda-calculus", Barendregt, Barendsen
19. nozione di proprietà di programmi; sistemi di tipo come
    approssimazioni modulari di proprietà di programmi
20. lambda calcolo tipato semplice: tipi, contesti, regole di tipaggio
21. algoritmo di unificazione
22. algoritmo di inferenza di tipo
23. teorema di subject reduction
24. teorema di normalizzazione forte per il lambda-calcolo tipato semplice
    # "Proofs as Types", Girard, Taylor, Lafont
25. isomorfismo di Curry-Howard
26. tipi corrispondenti ai connettivi della logica proposizionale e relativi
    termini
27. la quantificazione universale al secondo ordine come polimorfismo uniforme
    (cenni al System F)
28. la quantificazione esistenziale al secondo ordine come tipi di dato astratti