Il corso presenta i concetti e le tecniche che sono centrali in uno studio fondazionale dei linguaggi di programmazione, insieme con le loro basi logiche e formali. Il filo centrale consiste nel vedere i tipi e la semantica di un linguaggio come le strutture portanti, che ne determinano sia lo stile di programmazione che le proprietà’ formali dei programmi.
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
Altre Informazioni
La frequenza delle lezioni è fortemente consigliata.
Come strumento didattico è utilizzata la piattaforma e-learning di UNIFI: https://e-l.unifi.it/.
Ricevimento studenti: su appuntamento.
Il docente è contattabile per email: venneri@unifi.it .
Modalità di verifica apprendimento
Attività di seminari da parte degli studenti. Esame orale finale.
Programma del corso
1) Preliminari: definizioni induttive e metodi formali di prova.
2) Semantica operazionale strutturata. Introduzione ai sistemi di tipo: decidibilità. Le referenze imperative e la memoria.
2) Programmare con funzioni: Il lambda-calcolo tipato semplice. Semantica strict e semantica lazy. Ricorsione. Strategie di riduzione. Estensioni. Tipi per funzioni di ordine superiore. Prova di type-safety.
3) Sistemi di tipo polimorfi: metateoria del sottotipo. Inferenza di tipo e polimorfismo parametrico. Algoritmi di type-checking.
3) Caso di studio: Featherweight Java (un modello di Java). I tipi generici. La prova di type-safety. Tipi intersezione e wildcard.
4) Programmazione funzionale: ML e Python a confronto, type-checking dinamico e statico, strutture dati infinite.
4) Lambdas in Java8 : problemi di tipo.