Semantica (2007/2008)

Obiettivi formativi

Scopo del corso è quello di introdurre le principali tecniche matematiche usate nello studio dei linguaggi di programmazione:

* sistemi di tipi
* semantica operazionale
* domini
* semantica denotazionale

Il corso si rivolge a studenti con uno spiccato interesse per l'informatica teorica.

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 principi di induzione
2.1 induzione matematica, strutturale e ben fondata
2.2 induzione sulle derivazioni
2.3 definizioni per induzione
3 definizioni induttive
3.1 regole e induzione
3.2 regole di prova per la semantica operazionale
3.3 operatori e punti fissi
4 semantica denotazionale linguaggi imperativi
4.1 semantica denotazionale
4.2 confronto con la semantica operazionale
4.3 ordini parziali completi (cpo)
4.4 teorema del punto fisso
5 introduzione alla teoria dei domini
5.1 costruzione di cpo
5.2 un metalinguaggio per la teoria dei domini
6 linguaggi tipati
6.1 tipi
6.2 un linguaggio call-by-value: semantica operazionale e denotazionale
6.3 un linguaggio call-by-name: semantica operazionale e denotazionale
6.4 confronto delle semantiche operazionali e denotazionali

L'esame consiste in una prova scritta