STT - Semantica e Teoria dei Tipi

Docente

Ugo Montanari

Orario Lezioni

Finalita' del Corso

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.

Course Overview

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

• 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

Course Program

• 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

Libro di Testo/Textbook

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

Orario Recupero

Da fissare.

Appunti di Algebre come Categorie di Funtori

Vedi http://www.di.unipi.it/~ugo/algebras.pdf.

Appunti di pi-calcolo

Vedi http://www.di.unipi.it/~ugo/picalcolo.pdf

Modalita' d'Esame

Da definire caso per caso.

Last modified: 12-Oct-11

E_mail: ugo@di.unipi.it