Fondamenti - LINGUAGGI (2016/2017)

Codice insegnamento
4S02789
Docente
Massimo Merro
crediti
6
Settore disciplinare
INF/01 - INFORMATICA
Lingua di erogazione
Italiano
Sede
VERONA
Periodo
I sem. dal 3-ott-2016 al 31-gen-2017.
Pagina Web
http://profs.scienze.univr.it/~merro/linguaggi.html

Per visualizzare la struttura dell'insegnamento a cui questo modulo appartiene, consultare * organizzazione dell'insegnamento

Orario lezioni

Obiettivi formativi

L'obiettivo del corso è quello di presentare le basi teoriche dei linguaggi di programmazione. A tale scopo verranno introdotti vari linguaggi sequenziali paradigmatici, anche di ordine superiore. Il corso sarà incentrato sui concetti di semantica operazionale e di sistema di tipo. Verranno introdotte alcune tecniche formali per la verifica del comportamento dei programmi.

Al termine dell'insegnamento lo studente dovrà dimostrare di essere in grado di:
* definire, attraverso regole di inferenza, semantiche operazionali e sistemi di tipo per semplici linguaggi imperativi, funzionali e concorrenti;
* provare formalmente proprietà su un'arbitraria semantica operazionale usando tecniche diverse di induzione (matematica, strutturale, rule-based);
* conoscere e usare diverse nozioni di equivalenze semantica per confrontare il comportamento frammenti di programmi scritti in linguaggi imperativi, funzionali e concorrenti.

Programma

Lezioni frontali & Esercitazioni (56 ore)

• Introduction.
Transition systems. The idea of structural operational semantics. Transition semantics of a simple imperative language. Language design options. Exercises.
• Types.
Introduction to formal type systems. Typing for the simple imperative language. Statements of desirable properties.
• Induction. Exercises.
Review of mathematical induction. Abstract syntax trees and structural induction. Rule-based inductive definitions and proofs. Proofs of type safety properties. Exercises.
• Functions.
Call-by-name and call-by-value function application, semantics and typing. Local recursive definitions. Exercises.
• Data.
Semantics and typing for products, sums, records, references. Exercises.
• Subtyping.
Record subtyping and simple object encoding. Exercises.
• Semantic equivalence.
Semantic equivalence of phrases in a simple imperative language, including the congruence property. Examples of equivalence and non-equivalence. Exercises.
• Concurrency.
Shared variable interleaving. Semantics for simple mutexes; a serializability property. Exercises.



Testi di riferimento
Autore Titolo Casa editrice Anno ISBN Note
Peter Sewell Semantics of Programming Languages (Edizione 6) Cambridge University Press 2019 Note a cura del Prof. Sewell.
G. Winskel The formal Semantics of Programming Languages MIT Press 1993
Benjamin Pierce Types and Programming Languages (Edizione 1) MIT Press 2002 ISBN-10: 0262162091 Guida ineguagliabile per lo studio dei sistemi di tipi per i linguaggi di programmazione.

Modalità d'esame

L'esame consiste in una prova scritta composta da 4 o 5 esercizi. Lo svolgimento corretto di tutti gli esercizi consente di conseguire una votazione di 30/30.

Opinione studenti frequentanti - 2016/2017