| | | corso | | | | |
Semantica e teoria dei tipi
Codice: | 388AA | Crediti: | 6 | Semestre: | 2 | Sigla: | STT | |
|
Settore disciplinare: | INF/01 - Informatica |
Docente
Ugo Montanari
Tel. 0502212721Ultima versione disponibile: programma da confermare per l’a.a. 2012/2013
Prerequisiti
Elementi di base di logica e algebra.
Obiettivi di apprendimento
Verranno presentate alcune proprieta' 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.
Descrizione
English Description
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.
Programma
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 Calculus for Communicating Processes (CCS) e il Pi-calcolo di Milner e i loro modelli bialgebrici
Simply typed lambda calculus
Curry-Howard isomorphism
PCF and its cpo model, with applications to functional programming languages
Elements of recursive and polymorphic types, with applications to object oriented programming languages
Categories as partial algebras
Monoidal, cartesian and cartesian closed (CCC) categories
CCC as models of simply typed lambda calculus
Algebraic specifications, categories of models and adjunctions
Petri nets and their (strictly) symmetric monoidal models
Labelled Transition Systems (LTS) as coalgebras
Compositional LTS as bialgebras
Milner Calculus for Communicating Processes (CCS) and Pi-Calculus and their bialgebraic models
Bibliografia
John Mitchell, "Foundations for Programming Languages", MIT Press, 1996. Capitoli: 2.5,4,5,7.2,9,10,11.