Docenti

Prof. Pietro Di Gianantonio pietro.digianantonio@uniud.it http://www.dimi.uniud.it/pietro
Prof. Marino Miculan marino.miculan@uniud.it http://www.dimi.uniud.it/miculan

Crediti

12 CFU

Finalità

Scopo del corso è fornire le basi e gli strumenti per la definizione e lo studio della semantica dei linguaggi di programmazione, sia tradizionali (imperativi e funzionali), sia quelli più recenti contenenti gli aspetti di comunicazione, sicurezza e mobilità tipiche del calcolo globale.
Allo scopo vengono presentati una serie di linguaggi di programmazione con differenti caratteristiche e differenti livelli di complessità.
Per ciascun linguaggio vengono definite le appropriate semantiche (denotazionali e/o operazionali strutturate), e gli strumenti formali per la loro applicazione alla verifica di proprietà dei sistemi.

Programma

Il corso è diviso in due moduli.

1. Semantica dei sistemi sequenziali e concorrenti (6 CFU)

- Semantica di un semplice linguaggio imperativo.
- Domini per la semantica denotazionale: ordini, reticoli, teoremi di punto fisso. La teoria dei domini, domini base e costruttori di dominio.
- Semantica denotazionale di linguaggi funzionali con meccanismi di valutazione call by name e call by value.
- Teoria della ricorsione, teorema di Bekic e induzione di punto fisso.
- Semantica denotazionale tramite continuazioni di un linguaggio imperativo con environment, store, chiamate di procedura ed eccezioni.
- Linguaggi concorrenti: CSP, CCS, sistemi di transazione etichettati, la relazione di bisimulazione, logica di Hennessy-Milner.

2. Semantica dei sistemi distribuiti, sicuri e mobili (6 CFU)

- Sistemi concorrenti a topologia dinamica: il π-calcolo. Sintassi, semantica operazionale late e early, bisimulazioni late, early, open. Cenni a Pict.
- Sistemi per la sicurezza: lo spi-calcolo. Sintassi, semantica operazionale, verifica di proprietà di sicurezza mediante bisimulazioni. Il tool ProVerif.
- Sistemi per la mobilità: il calcolo degli ambienti mobili. Sintassi, semantica operazionale, logica modale spaziale, sistemi di tipi. Varianti e applicazioni.
- Metamodelli per i sistemi concorrenti e distribuiti: i bigrafi.

Bibliografia

- Glynn Winskel. The formal semantics of programming languages. MIT Press, 1993.
- Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, Jiri Srba. Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007.
- Articoli e dispense dei docenti

Modalità d'esame

Esame scritto ed orale (I modulo); approfondimento su un argomento del corso (II modulo).