Insegnamento mutuato da: B012511 - TEORIA DEI LINGUAGGI DI PROGRAMMAZIONE Laurea Magistrale in INFORMATICA
Contenuto del corso
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
Modalità di verifica apprendimento
Attività di seminari da parte degli studenti. Esame orale finale.
Programma del corso
Il programma si articola nei seguenti punti.
1) Fondamenti: semantica operazionale strutturata; sistemi di tipo e algoritmi di type-checking, proprietà’ di type-safety.
2) Programmazione funzionale: il lambda-calcolo tipato semplice. Semantica stretta e lazy. Introduzione del polimorfismo per sottotipo. Tipi parametrici algoritmi di deduzione del tipo.
3) Caso di studio: due linguaggi a confronto.
(1) Featherweight Java, una restrizione di Java alla sua parte più’ significativa. Il type-checking statico. Uso dei tipi Generici. Semantica stretta. Safety dei programmi.
(2) Il linguaggio Python. Il type-checking dinamico. Stile di programmazione con funzioni di ordine superiore. Funzioni con semantica lazy.