elenco    
        corso    

Modelli di calcolo (Principles for software composition)

Codice: 375AACrediti: 9Semestre: 2Sigla: MOD 
 
Settore disciplinare: INF/01 - Informatica

Docente

Ugo Montanari   ugo@di.unipi.it  Stanza 280  Tel. 0502212721

Prerequisiti

Una conoscenza elementare di logica e algebra.

Obiettivi di apprendimento

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.

Descrizione

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.

English Description

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.

Programma

    •    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)
(in English)
    •    Introduction and proof systems based on inference rules. (2h)
    •    Syntax and operational semantics of a simple imperative programming language (IMP). (4h)
    •    Induction proof principles. (4h)
    •    Domains and minimal fixpoint theorem. (4h)
    •    Immediate consequences operator and its fixpoint. (2h)
    •    Denotational semantics of IMP. (2h)
    •    Equivalence between operational and denotational semantics of IMP. (4h)
    •    Syntax and lazy operational semantics of a functional, higher order programming language (HOL). (4h)
    •    Domain constructions. (2h)
    •    Lazy denotational semantics of HOL. (2h)
    •    Relation between operational and denotational semantics of HOL. (2h)
    •    Syntax and operational semantics of CCS. (4h)
    •    Observational semantics of CCS. (4h)
    •    Temporal and modal logics: HM, LTL, CTL*, mu-calculus. (6h)
    •    Syntax and operational semantics of pi-calculus. (4h)
    •    Observational semantics of pi-calculus. (4h)
    •    Operational models with discrete probabilities, Markov processes. (4h)
    •    Probabilistic automata (PA). (2h)
    •    Bisimulation and Hennessy-Milner logic on PA. (2h)
    •    Syntax and semantics of PEPA. (2h)
Ore lezione: 50Ore esercitazione: 20Ore laboratorio: 0Ore seminari: 0 

Bibliografia

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.

Modalità di esame

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.



Ulteriore pagina web del corso: http://www.di.unipi.it/~ugo/MOD.html


home


email