Dottorato di Ricerca in Informatica - XII ciclo
Semantica Operazionale e Denotazionale dei linguaggi di programmazione
prof. Rocco De Nicola, Università di Firenze
Programma preliminare del corso
Definizione di funzioni e lambda-notazione
Semantica denotazionale e definizione di funzioni, la
lambda--notazione e la semantica delle definizioni ricorsive. Domini per la
semantica denotazionale: insiemi parzialmente ordinati completi e teorema
del minimo punto fisso, costruzioni di domini, sistemi di equazioni
mutuamente ricorsive.
Semantica di linguaggi di programmazione sequenziale
Semantica di un semplice linguaggio funzionale: il metalinguaggio;
semantica operazionale, semantica denotazionale e loro relazioni. Semantica
di linguaggi imperativi: una calcolatrice tascabile, il linguaggio Tiny.
Semantica diretta e con continuazioni di linguaggi con contesti: il
linguaggio Small.
Nondeterminismo e Concorrenza
Linguaggi di programmazione concorrente e meccanismi di
comunicazione diretta ed indiretta; programmazione nondeterministica
imperativa: "Guarded Commands", processi comunicanti: OCCAM - CSP;
programmazione concorrente applicativa: CCS.
Testi di Riferimento
- R. De Nicola, Semantica Operazionale e Denotazionale dei Linguaggi di
Programmazione. Note 1997.
- R. De Nicola, V. Manca, U. Montanari, F. Turini, Semantica Denotazionale
ed Algebrica dei Linguaggi di Programmazione, FRANCO ANGELI, 1989.
- G. Winskel, The Formal Semantics of Programming Languages: An
Introduction; Mit Press, 1993.