Semantica e Concorrenza

Corso di Laurea Magistrale in Informatica

Docenti

Finalità del corso

Obiettivo del corso è quello di fornire le conoscenze fondamentali sulle principali tecniche utilizzate per descrivere formalmente la semantica dei linguaggi di programmazione; insegnare come modellare i diversi aspetti del calcolo: ordine superiore, non determinismo, concorrenza; insegnare le principali problematiche dei sistemi concorrenti e distribuiti. Questa conoscenza viene applicata alla prova formale della proprietà dei programmi. Inoltre, lo studente impara ad essere consapevole delle ambiguità presenti nelle descrizioni informali e descrivere formalmente il comportamento dei costruttori di linguaggi di programmazione.

Programma del CORSO

Gli argomenti trattati sono i seguenti: 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. Descrizione e analisi di algoritmi di mutua esclusione mediante processi CCS. Un linguaggio per processi mobili: pi-calcolo. Semantica operazionale mediante sistema di transizione etichettato e sistema di riduzione, bisimilarità e congruenze.

Libri di testo

Glyn Winskel. The formal semantics of programming languages. MIT Press.
Luca Aceto, Anna Ingolfsdottir, Kim G. Larsen, J. Srba. Reactive Systems. Cambridge University Press, 2007.

Lucidi presentati a lezione

Module di Semantica: Lucidi in formato pdf: [1 per pagina], [ 4 per pagina].

Modalità di svolgimento dell'esame

L'esame si compone di un progetto e di una prova orale. Il progetto, assegnato su appuntamento e da svolgere entro una settimana, prevede alcuni esercizi, relativamente complessi. La prova orale consiste in una discussione del progetto e in una serie di domande di teoria.