Semantica
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.
Attività Formativa
L'attività formativa sarà basata su lezioni frontali.
Programma
-
Il concetto di semantica dei linguaggi di
programmazione: il caso di un semplicissimo linguaggio
imperativo
-
Il lamda-calcolo tipato semplice:
sintassi e semantica
-
Il linguaggio PCF (Programming Language for Computable Functions)
-
Semantica operazionale di PCF: Call-by-Value
-
Ordini parziali completi (CPO) e punti fissi
-
Semantica a Punto-Fisso di PCF
-
Confronto tra semantica operazionale e
semantica denotazionale
- Call-by-Value per PCF
- Polimorfismo
-
Il sistema polimorfo di tipi di ML
-
Il sistema di inferenza dei tipi
-
Il lambda-calcolo polimorfo: sistema F
di Girard (cenni)