Prof. Ugo Montanari

Modelli di Calcolo di Sistemi Funzionali, Concorrenti e Interattivi

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.

Programma:

1. Il lambda calcolo con tipi semplici
2. L'isomorfismo di Curry-Howard
3. Il PCF e il suo modello cpo, con applicazione ai linguaggi di programmazione funzionali
4. Elementi di tipi ricorsivi e polimorfi, con applicazione ai linguaggi di programmazione orientati agli oggetti
5. Le categorie come algebre parziali
6. Categorie monoidali, cartesiane e cartesiane chiuse (CCC)
7. Le CCC come modelli del lambda calcolo con tipi semplici
8. Specifiche algebriche, categorie di modelli e aggiunzioni
9. La semantica operazionale come costruzione universale
10. Le reti di Petri e i loro modelli monoidali (strettamente) simmetrici
11. I sistemi di riscrittura etichettati (LTS) come coalgebre
12. I sistemi LTS composizionali come bialgebre
13. Il Calculus for Communicating Processes (CCS) di Milner e i suoi modelli bialgebrici.
14. Il pi-calcolo e i fondamenti algebrici dei calcoli nominali.

Periodo di svolgimento
1 febbraio 2010 - 31 maggio 2010
Numero di ore di lezione: 40
Numero di ore settimanali di lezione: 4

Modalità dell'esame
Prova orale e seminari

Prerequisiti e anni di corso per cui è consigliato
Una conoscenza elementare di logica e algebra.
Quarto-quinto anno

Eventuali riferimenti bibliografici
Mitchell, Semantics of Programming Languages, MIT Press, 1996, capitoli 2.5,4,5,7.2,9,10,11.
Note manoscritte.