Argomenti e risultati fondamentali nella teoria dei linguaggi di programmazione: semantica operazionale strutturata e relativi metodi formali di prova, sistemi di tipo. Linguaggi funzionali e funzioni di ordine superiore, teorie di tipi semplici e polimorfi. Il sottotipo nei linguaggi orientati agli oggetti. Algoritmi di type-checking. Problemi di interpretazione dei linguaggi.
Testo di riferimento:
Types and Programming Languages. Benjamin C. Pierce.
The MIT Press, Cambridge, Massachusetts.
http://mitpress.mit.edu, ISBN 0-262-16209-1
Altro materiale, basato su articoli di ricerca, sarà fornito per lo svolgimento degli approfondimenti e seminari da parte degli studenti e incluso nell'esame.
Obiettivi Formativi
Conoscenze acquistite (al termine del corso):
Argomenti di base dei Linguaggi di Programmazione, dal modello funzionale a quello orientato agli oggetti.
Competenze acquisite (al termine del corso).
Gli studenti dovranno 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 proprietà di linguaggi e di programmi, di definire e implementare algoritmi di type-checking, di utlizzare in modo adeguato i costrutti principali di linguaggi avanzati.
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) 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
Corsi su metodi formali sono utii. Una buona esperienza di programmazione è richiesta.
Metodi Didattici
Strategie di apprendimento "attivo" sono incorporate in ciascuna componente della progettazione del corso. Pertanto diverse metodologie didattiche sono integrate fra loro:
a) Lezioni frontali
b) Sviluppo interattivo di esercizi in classe
c) Compiti e Seminari assegnati agli studenti. Ogni studente, o gruppo di 2-3 studenti, avrà assegnato uno specifico argomento da approfondire; quindi, gli studenti presenteranno in aula il loro approfondimento e guideranno la successiva discussione.
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
L'esame finale del corso è un colloquio orale individuale.
Il voto finale è determinato da una media pesata dei punteggi ottenuti nell'esame finale e negli argomenti di approfondimento con seminario, secondo la seguente partizione (indicativa e soggetta a possibili modifiche) :
40% approfondimento e seminario, 60% esame finale.
Programma del corso
Il corso presenta i concetti e le tecniche centrali della Teoria dei Linguaggi di programmazione, insieme con le loro basi logiche e formali. La semantica operazionale e i sistemi di tipo più avanzati sono presentati considerando le loro principali applicazioni all’ingegneria del software, al design dei linguaggi ed alle proprietà di sicurezza. L’intento è pragmatico: le caratteristiche dei più diffusi linguaggi di programmazione (come C++, Java e Python) sono messe a confronto con motivazioni pratiche, includendo le proprietà di "safety".
Argomenti principali.
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.
3) 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.
4) Sistemi di tipo polimorfi: metateoria del sottotipo. Inferenza di tipo e polimorfismo parametrico. Algoritmi di type-checking.
5) Caso di studio: Featherweight Java (un modello di Java). I tipi generici. La prova di type-safety. Tipi intersezione e wildcard.
6) Programmazione funzionale: ML e Python a confronto, type-checking dinamico e statico, strutture dati infinite.
7) Lambdas in Java8 : problemi di tipo.
8) Applicazioni: confronto di diversi linguaggi di programmazione (Java, C++, Python, Haskell) rispetto alle caratteristiche principali derivanti sia dalla semantica che dal sistema di tipo.