Sillabo dell'insegnamento

• A - Fondamenti
V - Varie
richiami su logica booleana e del primo ordine, tecniche per dimostrare correttezza/terminazione di algoritmi (visti come sistemi di transizione deterministici)
* CAL - Calcolabilita'
Modelli di calcolo (TM e RAM), funzioni calcolabili, complessita' tempo e spazio, relazioni tra modelli di calcolo, Tesi di Church
* CAL - Calcolabilita'
problemi/linguaggi decidibili e semidecidibili, riducibilita' tra problemi, codifica delle TM, funzione e TM universale
* CAL - Calcolabilita'
esempi di problemi non (semi)decidibili, proprieta' di chiusura dei linguaggi (semi)decidibili
COM - Complessita'
classi di complessita' (tempo/spazio e deterministico/non-deterministico) e relazioni tra classi di complessita'
COM - Complessita'
classi naturali di complessita' (L, NL, P, NP, PSPACE), teorema di Cook, esempi di problemi NP-completi
SLP - Semantica dei Linguaggi di Programmazione
Semantica operazionale small-step, sistemi di tipo, soundness
SLP - Semantica dei Linguaggi di Programmazione
Lambda-calcolo non tipato e tipato semplice
SLP - Semantica dei Linguaggi di Programmazione
Estensioni del lambda calcolo tipato: let, ricorsione, costrutti imperativi, eccezioni
SLP - Semantica dei Linguaggi di Programmazione
Featherweight Java, cenni di semantica denotazionale
L - Logica
Definizioni induttive e prove per induzione, induzione strutturale, asserzioni alla Hoare
L - Logica
Sistema di Hoare per la correttezza parziale e totale