Insegnamento mutuato da: B012511 - TEORIA DEI LINGUAGGI DI PROGRAMMAZIONE Laurea Magistrale in INFORMATICA
Contenuto del corso
Il corso presenta i concetti e le 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 proprietà. Argomenti centrali sono: tecniche di semantica operazionale per la definizione formale dei linguaggi, sistemi di tipo e proprietà di correttezza, polimorfismo e sottotipo, fondamenti dei linguaggi orientati
Types and Programming Languages. Benjamin C. Pierce. MIT Press, 2002.
Obiettivi Formativi
Alla fine del corso, gli studenti dovranno aver acquisito le seguenti competenze:
1) Un approccio rigoroso, basato sulla teoria dei tipi, allo studio di problemi connessi al design di linguaggi, alle loro estensioni e implementazioni.
2) Capacità di usare tecniche formali di prova per studiare le proprietà dei programmi.
3) Una preparazione sufficientemente profonda (su semantica e tipi) da consentire l'approfondimento di pubblicazioni di ricerca sui temi trattati.
Prerequisiti
Prerequisiti raccomandati: Metodi Formali. Corsi avanzati di programmazione. Logica matematica.
Metodi Didattici
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
Modalità di verifica apprendimento
Attività di seminari da parte degli studenti. 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 proprietà con tecniche rigorose.
Il programma del corso si articola nei seguenti punti:
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 disottotipo.Algoritmidi 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.