Semantica dei linguaggi di programmazione - Programming Language Semantics

Programma dell'insegnamento - Corso di laurea in Informatica Magistrale

Docente

Prof. Pietro Di Gianantonio

Indirizzo e-mail
pietro.digianantonio@uniud.it

Indirizzo Pagina Web Personale

http://www.dimi.uniud.it/pietro

Crediti

6 CFU

Finalità

Obiettivo della semantica dei linguaggi di programmazione è lo sviluppo di metodi per definire in maniera formale e rigorosa il comportamento di programmi. Questi metodi possono quindi essere applicare per ragionare sui programmi, provarne la loro correttezza o il rispetto di determinati vincoli durante la loro esecuzione.

Scopo del corso è fornire le nozioni fondamentali della semantica dei linguaggi di programmazione.

A questo fine vengono presentati una serie di linguaggi di programmazione con differenti caratteristiche e differenti livelli di complessità.

Per ciascun linguaggio vengono definite le appropriate semantiche (denotazionali e/o operazionali strutturate), e gli strumenti formali per la loro applicazione alla verifica di proprietà dei programmi.

Programma

- Semantica di un semplice linguaggio imperativo.

- Domini per la semantica denotazionale: ordini, reticoli, teoremi di punto fisso. La teoria dei domini, domini base e costruttori di dominio.

- Semantica denotazionale di linguaggi funzionali con meccanismi di valutazione call by name e call by value.

- Teoria della ricorsione, teorema di Bekic e induzione di punto fisso.

- Semantica denotazionale tramite continuazioni di un linguaggio imperativo con environment, store, chiamate di procedura ed eccezioni.

- Linguaggi concorrenti: CSP, CCS, sistemi di transazione etichettati, la relazione di bisimulazione, logica di Hennessy-Milner.

Bibliografia

- Glynn Winskel. The formal semantics of programming languages. MIT Press.

- Dispense de docente.

Modalità d'esame

Esame scritto ed orale.

************************************************************************************

Aims

Aim of the course is to give an introduction to the semantics of programming languages.

A series of programming languages with different features and different levels of complexity are presented. For each language, the appropriate semantics and formal tools and techniques for their applications are given.

Program

- Semantics of a simple imperative language.

- Domains for denotational semantics: partial orders, lattices, fixed-point theorems. Domain theory, basic domains and domain constructors.

- Operational and denotational semantics of functional programming languages with call by value and call by name evaluation mechanisms.

- Recursion theory, Bekic theorem, and fixed-point induction.

- Continuation semantics of imperative programming languages with environment, store, procedure calls and exceptions.

- Concurrent languages: CSP, CCS. Label transitions systems.

bisimulation relation, Hennessy-Milner logic.

Bibliography