Semantica e teoria dei tipi

Ugo Montanari      Tel. 0502212721

Accorpamento con Corso della Scuola Normale

Nell'anno accademico 2010-2011 il Corso verra' tenuto presso la Scuola Normale con il titolo "Modelli di Calcolo di Sistemi Funzionali, Concorrenti e Interattivi" (vedi http://www.sns.it/it/scienze/matematiche/modcal/). Il Corso potra' essere comunque seguito ed accreditato per l'Universita' di Pisa.


Orario

Le lezioni inizieranno mercoledi' 9 marzo ore 11-12 in aula Tonelli alla Scuola Normale.
A partire dal giovedi' 17 marzo le lezioni saranno, sempre presso la Scuola Normale:

- Giovedì in aula Tonelli dalle 11.00 alle 13.00
- Venerdì in aula Mancini dalle 11.00 alle 13.00

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.