Concetti e tecniche fondamentali in un approccio fondazionale ai linguaggi di programmazione. Il filo centrale consiste nel vedere sia un singolo programma che un linguaggio completo come un oggetto matematico, sul quale si possono asserire e provare precise proprieta'. Argomenti centrali sono: tecniche di semantica operazionale per la definizione formale dei linguaggi, sistemi di tipo e proprieta' di correttezza, polimorfismo e sottotipo, fondamenti dei linguaggi orientati agli oggetti.
Types and Programming Languages. Benjamin C. Pierce. MIT Press, 2002.
Obiettivi Formativi
Conoscenze:
Argomenti e risultati fondamentali nella teoria dei linguaggi di programmazione: semantica operazionale e relativi metodi formali di prova, sistemi di tipo per modelli imperativi, funzionali e orientati agli oggetti. Problemi di implementazione.
Competenze acquisite
Gli studenti dovranno dimostrare di essere in grado di definire formalmente la semantica operazionale e il sistema di tipo di un linguaggio “core”, di progettare estensioni a nuovi costrutti, di usare tecniche formali per provare le relative proprieta', di definire e implementare algoritmi di type-checking.
Capacità acquisite al termine del corso:
1) Un approccio rigoroso, basato sulla teoria dei tipi, allo studio di problemi connessi al design di linguaggi, alle loro estensioni e implementazioni.
2) Capacita' di usare tecniche formali di prova per studiare le proprieta' dei programmi.
3) Una preparazione sufficientemente profonda (su semantica e tipi) da consentire l'approfondimento di pubblicazioni di ricerca sui temi trattati.
Prerequisiti
Corsi raccomandati: Modelli di Sistemi Sequenziali e Concorrenti
Metodi Didattici
Numero di ore totali del corso: 150
Numero di ore per studio personale e altre attività formative di tipo individuale: 90
Numero di ore relative alle attività in aula: 48
Numero di ore relative ad attività seminariali: 12
Altre Informazioni
Orario di ricevimento
Martedi', 15.00 – 17.00
Modalità di verifica apprendimento
Modalità:
Attivita' di seminari e esame orale finale.
Programma del corso
Il corso presenta i concetti e le tecniche centrali in uno studio fondazionale dei linguaggi di programmazione, insieme con le loro basi logichee formali. Il filo centrale consiste nel vedere sia un singolo programma che un linguaggio completo come un oggetto matematico, sul quale si possono asserire e provare precise proprieta' con tecniche rigorose.
1) Fondamenti- Programmazione funzionale, definizioni induttive e metodi formali di prova. Semantica operazionale.
2) Sistemi di tipo- Il lambda-calcolo tipato semplice, le referenze imperative e la type-safety. La metateoria della definizione di sottotipo. Algoritmi di type-checking. Polimorfismo e inferenza di tipo.
3) Caso di studio: Featherweight Java (un modello del cuore di java). I tipi generici. La prova di Safety. Tipi intersezione e wildcard.
4) Argomenti avanzati, come i tipi esistenziali e/o il polimorfismo di ordine superiore.