Modelli di calcolo (Principles for software composition)

Ugo Montanari      Tel. 0502212721

Una conoscenza elementare di logica e algebra.

La presentazione di quattro modelli di calcolo (imperativo: IMP, funzionale: HOFL, per processi: CCS, nominale: pi-calcolo) con principi di induzione e metodi di prova.

Vengono introdotti i principi della semantica operazionale, della semantica denotazionale e delle tecniche per metterle in relazione per un linguaggio imperativo e per un linguaggio funzionale di ordine superiore. Viene anche presentata la semantica operazionale e osservazionale di due calcoli per la descrizione di processi (CCS e pi-calcolo). Infine si esaminano i modelli operazionali con probabilità discrete e li si presentano dal punto di vista degli automi probabilistici.

We introduce 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. Operational and observational semantics of two process description languages (CCS and pi-calculus) is also presented. Finally, we consider operational nondeterministic models with discrete probabilities, and we present them from the perspective of probabilistic automata.

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

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.

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