Modelli di calcolo (Principles for software composition)

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.