Semantica e teoria dei tipi

Ugo Montanari      Tel. 0502212721

Il corso intende presentare alcuni concetti essenziali dell'informatica, quali tipi, applicazione funzionale, concorrenza, interazione, nella forma astratta correntemente considerata standard. Il corso sostituisce quello di "Fondamenti dell'Informatica: Semantica II" offerto negli anni precedenti.

Verranno presentate alcune proprietà fondamentali dei modelli di calcolo, come la semantica operazionale ed astratta, la struttura dei tipi, l'ordine superiore, la concorrenza, l'interazione. Verranno utilizzate la semantica algebrica e la teoria elementare dei tipi, ma non vi sono prerequisiti eccetto una conoscenza elementare dell'algebra e della logica.

Some basic properties of models of computation are studied, like operational and abstract semantics, typing, higher order, concurrency, interaction. Algebraic semantics and elementary category theory are employed, but no prerequisites are required except for some elementary knowledge of logic and algebra.

Il lambda calcolo con tipi semplici. L'isomorfismo di Curry-Howard. Il PCF e il suo modello cpo, con applicazione ai linguaggi di programmazione funzionali. Elementi di tipi ricorsivi e polimorfi, con applicazione ai linguaggi di programmazione orientati agli oggetti. Le categorie come algebre parziali. Categorie monoidali, cartesiane e cartesiane chiuse (CCC). Le CCC come modelli del lambda calcolo con tipi semplici. Specifiche algebriche, categorie di modelli e aggiunzioni. Le reti di Petri e i loro modelli monoidali (strettamente) simmetrici. I sistemi di riscrittura etichettati (LTS) come coalgebre. I sistemi LTS composizionali come bialgebre. Il CCS di Milner e i suoi modelli bialgebrici. Il pi-calcolo e i sui modelli di coalgebre in una categoria di presheaf.

John Mitchell, "Foundations for Programming Languages", MIT Press, 1996, capitoli: 2.5,4,5,7.2,9,10,11. Materiale distribuito a lezione.

Un esame orale o la preparazione di un seminario su argomenti attinenti il corso, da definire caso per caso.