MOD - Modelli di Calcolo

Docente

Orario del Corso

Vedi web del Dipartimento

Verifiche Intermedie ed Esami

Le soluzioni delle prove scritte sono disponibili presso la pagina dei testi d'esame.

La correzione dello scritto del 10/02/2014 e una sessione di orali avranno luogo venerdì 14 febbraio ore 09:00 presso lo studio del docente.

L'ultima sessione d'orali dell'appello avrà luogo mercoledì 26 c.m. alle ore 9 presso lo studio del docente. Si ricorda che con questo appello scade la validità degli scritti dell'intero anno accademico.

In entrambi i casi gli interessati sono pregati di inviare una email a ugo@di.unipi.it.

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.

Note a Stampa

Roberto Bruni, Lorenzo Galeotti, Ugo Montanari

Models of Computation - Part I-V

Introduction, Preliminaries, Operational Semantics of IMP, Induction, Recursion, Partial Orders, Denotational Semantics of IMP, Operational Semantics of HOFL, Domain Theory, Denotational Semantics of HOFL, CCS, Temporal Logic, Mu-calculus, Pi-calculus, Markov Chains with Actions and Nondeterminism, PEPA

Modalità d'Esame

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

Testi d'esame

Regole per compitini ed esami

Last modified: 10-Feb-14

E_mail: ugo@di.unipi.it