MOD - Modelli di Calcolo

Docente

Ugo Montanari

Orario del Corso

Vedi web dipartimento.

Sessioni di Esami Orali

La correzione del compito del 01/02/12 e i  prossimi orali avranno luogo il lunedì 06/02/12 alle ore 09:00 presso l'aula N1.

Il testo della correzione del compito del 01/02/2012 è disponibile presso http://www.di.unipi.it/~ugo/010212 correction.pdf.

Finalita' del Corso

Il corso introduce i principi della semantica operazionale, i principi della semantica denotazionale e le tecniche per confrontarle nel caso di un linguaggio imperativo e di un linguaggio funzionale di ordine superiore. Vengono poi presentati due calcoli per la descrizione di processi, il CCS e il pi-calcolo. Infine vengono introdotti i sistemi di transizione probabilistici. 

Course Overview

We present the principles of operational semantics, the principles of denotational semantics, and the techniques to relate one to the other for an imperative language and for a higher order functional language. We also present two process calcoli, CCS and pi-calculus. Finally we introduce probabilistic transition systems. 

Programma Dettagliato

• Introduzione e sistemi di prova con regole di inferenza. (2h)
• Sintassi e semantica operazionale di un semplice linguaggio imperativo (IMP). (4h)
• Domini e costruzioni di domini. (4h)
• Teorema del minimo punto fisso. (2h)
• Segnature e algebre dei termini. (2h)
• Semantica denotazionale di IMP. (2h)
• Tecniche di prova per induzione. (4h)
• Equivalenza tra semantica operazionale e denotazionale di IMP. (4h)
• Sintassi e semantica operazionale lazy di un linguaggio funzionale higher order (HOL). (4h)
• Semantica denotazionale lazy di HOL. (2h) Relazione tra semantica operazionale e denotazionale di HOL. (2h)
• Sintassi e semantica operazionale del CCS. (4h)
• Semantica osservazionale del CCS. (4h)
• Logica di Hennessy-Milner. (2h)
• Sintassi e semantica operazionale del pi-calcolo. (4h)
• Semantica osservazionale del pi-calcolo. (4h)
• Modelli operazionali con probabilità discrete, processi di Markov, (4h)
• Automi probabilistici (PA). (2h)
• Simulazione e bisimulazione di PA. (2h)

Libro di Testo/Textbook

Glynn Winskel, "The formal Semantics of Programming Languages", MIT Press, 1993. Capitoli: 1.3, 2, 3, 4, 5, 8, 11. "La Semantica Formale dei Linguaggi di Programmazione", traduzione italiana a cura di Franco Turini, UTET 1999.
Robin Milner, "Communication and Concurrency, Prentice Hall, 1989. Capitoli: 1-7, 10.

Modalita' d'Esame

Due compitini durante l'anno. Una prova scritta di 3 ore, seguita da una prova orale.

Testi d'esame

Regole per compitini ed esami

Last modified: 03-Feb-12

E_mail: ugo@di.unipi.it