corso |
Codice: | 375AA | Crediti: | 9 | Semestre: | 2 | Sigla: | MOD | |
Settore disciplinare: | INF/01 - Informatica |
Una conoscenza elementare di logica e algebra.
La presentazione di cinque modelli di calcolo (imperativo: IMP, funzionale: HOFL, per processi: CCS, nominale: pi-calcolo e probabilistico/stocastico: automi di Segala e PEPA) 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 presentata la semantica operazionale e osservazionale di due calcoli per la descrizione di processi (CCS e pi-calcolo). Si illustrano anche alcune logiche temporali e modali (HM, LTL, CTL*, mu-calcolo). Infine si esaminano i modelli operazionali con probabilità discrete e li si presentano dal punto di vista degli automi probabilistici e stocastici e del calcolo PEPA.
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) are presented. Several examples of temporal and modal logics are also discussed (HM, LTL, CTL*, mu-calculus). Finally, we consider operational nondeterministic models with discrete probabilities, and we present them from the perspective of probabilistic and stochastic automata, and of the PEPA calculus.
• Introduzione e sistemi di prova con regole di inferenza. (2h)
• Sintassi e semantica operazionale di un semplice linguaggio di programmazione imperativo (IMP). (4h)
• Principi di prova per induzione. (4h)
• Domini e teorema del minimo punto fisso. (4h)
• Operatore delle conseguenze immediate e suo punto fisso. (2h)
• Semantica denotazionale di IMP. (2h)
• Equivalenza tra semantica operazionale e denotazionale di IMP. (4h)
• Sintassi e semantica operazionale lazy di un linguaggio di programmazione funzionale higher order (HOL). (4h)
• Costruzioni di domini. (2h)
• 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)
• Logiche temporali e modali (HM, LTL, CTL*, mu-calcolo). (6h)
• 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)
• Sintassi e semantica di PEPA. (2h)
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 alla fine. La prova scritta non è necessaria se si superano entrambi i compitini.