Fondamenti dell'Informatica: Semantica B

(Corso di Laurea in Informatica (quinquennale))

Codice:

4I040

Crediti:

Semestre:

Sigla:

Fse

Docente

Andrea Maggiolo Schettini

Tel. 0502212700

Prerequisiti

Programmazione, Matematica Discreta, Logica Matematica, Fondamenti dell'Informatica: Calcolabilità e Complessità

Obiettivi di apprendimento

Il corso presenta i principi della semantica operazionale, i principi della semantica denotazionale e le tecniche per confrontarle nel caso di un linguaggio imperativo e di un linguagggio funzionale di ordine superiore.

Descrizione

La prima parte del corso tratta i principi di induzione (ben fondata, sulle regole, strutturale), la semantica denotazionale e operazionale per un semplice linguaggio imperativo, e la prova della loro equivalenza. La seconda parte del corso affronta i fondamenti della semantica denotazionale e, in particolare, le algebre eterogenee ed i morfismi tra loro, gli ordinamenti parziali completi e i teoremi di punto fisso. La terza parte presenta la semantica operazionale, la semantica denotazionale e le loro relazioni per un linguaggio funzionale, tipato e di ordine superiore.

English Description

The course presents 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, typed functional language.

The first part deals with induction principles (well-founded induction, rule induction, structural induction), the operational and denotational semantics for a simple imperative language, and the proof of the equivalence of the semantics. The second part deals with the foundation of denotational semantics. The third part presents the operational and denotational semantics of a functional, higher order, typed language.

Programma

Introduzione e lambda-notazione (2h)
Semantica operazionale di un semplice linguaggio imperativo (IMP) (2h)
Principi di induzione (3h)
Ricorsione ben fondata (1h)
Ordinamenti parziali e teorema del minimo punto fisso (3h)
Domini e costruzioni di domini (4h)
Segnature e algebre dei termini (1h)
Semantica denotazionale di IMP (2h)
Equivalenza tra semantica operazionale e denotazionale di IMP (2h)
Semantica operazionale lazy di un linguaggio funzionale higher order(1h)
Semantica denotazionale lazy di un linguaggio funzionale higher order(2h)
Relazioni tra le due semantiche (2h)

Ore lezione:

Ore esercitazione:

Bibliografia

Glynn Winskel, "Semantica formale dei linguaggi di programmazione", UTET, 1999.