Il corso introduce le principali tecniche sviluppate nell'area della "semantica formale dei linguaggi di programmazione":
* sistemi di tipi
* semantica operazionale
* domini
* semantica denotazionale
Il corso presuppone le competenze acquisite nei corsi di "Programmazione", "Logica", "Algebra", "Linguaggi di Programmazione" e "Fondamenti dell'informatica" della laurea triennale in informatica.
1 semantica operazionale
1.1 definizione di un semplice linguaggio imperativo
1.2 regole di valutazione
2 induzione
2.1 induzione matematica
2.2 induzione strutturale
2.3 induzione ben fondata
3 semantica denotazionale dei linguaggi imperativi
3.1 composizionalita'
3.2 il caso dei programmi senza while
3.3 il trattamento del while
4 introduzione alla teoria dei domini
4.1 ordini parziali completi
4.2 continuita'
4.3 il teorema di Knaster-Tarski
4.4 costruzione di domini:
domini prodotto; domini di funzioni; domini piatti
5 PCF
5.1 termini e tipi
5.2 variabbili liberee legate; sostituzione
5.3 tipaggio
5.4 valutazione (semantica operazionale)
6 semantica denotazionale di PCF
6.1 denotazione dei termini
6.2 denotazione dei termini
6.3 composizionalita'
6.4 correttezza
L'esame consiste in una prova scritta