Semantica e teoria dei tipi

Ugo Montanari      Tel. 0502212721

Elementi di base di logica e algebra.

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.

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 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

John Mitchell, "Foundations for Programming Languages", MIT Press, 1996. Capitoli: 2.5,4,5,7.2,9,10,11.