Semantica (2004/2005)

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, di tipo prettamente teorico, si rivolge a studenti della laurea specialistica in informatica con forti interessi allo studio dei fondamenti dei linguaggi di programmazione.

Il corso presuppone le competenze acquisite nei corsi di "Programmazione", "Logica", "Algebra" e "Fondamenti dell'informatica" della laurea triennale in informatica.

1. Il concetto di semantica dei linguaggi di programmazione: il caso di un semplicissimo linguaggio imperativo
2. Il lamda-calcolo tipato semplice: sintassi e semantica
3. Il linguaggio PCF (Programming Language for Computable Functions)
1. Semantica operazionale di PCF: Call-by-Value
2. Ordini parziali completi (CPO) e punti fissi
3. Semantica a Punto-Fisso di PCF
4. Confronto tra semantica operazionale e semantica denotazionale
5. Call-by-Value per PCF
4. Polimorfismo
1. Il sistema polimorfo di tipi di ML
2. Il sistema di inferenza dei tipi
3. Il lambda-calcolo polimorfo: sistema F di Girard (cenni)

L'attività formativa sarà basata su lezioni frontali.

L'esame consiste in una prova orale