Il contenuto di questo corso consiste in uno studio approfondito della teoria dei linguaggi di programmazione, incluse le principali tecniche per l’analisi e l’implementazione dei linguaggi. Argomenti principali: semantica operazionale e dimostrazioni; funzioni di ordine superiore, lambda-calcolo e valutazione parziale; sistemi di tipo e prove di correttezza per linguaggi funzionali e orientati agli oggetti; polimorfismo; controllo di tipo statico e dinamico.
Testo di riferimento: Types and Programming Languages. Benjamin C. Pierce. MIT Press, 2002.
Materiale aggiuntivo, costituito da articoli di ricerca, sarà messo a disposizione per approfondimenti assegnati agli studenti.
Obiettivi Formativi
Al superamento di questo corso, lo studente sarà in grado in grado di
- definire formalmente la semantica operazionale e il sistema di tipo di un linguaggio “core”, progettare estensioni a nuovi costrutti
- usare tecniche formali per provare proprietà di un linguaggio o di un programma
- mettere a confronto, in modo critico, diversi linguaggi, spiegandone i concetti fondamentali, le caratteristiche, le differenze di desing con relativi vantaggi e svantaggi
- scegliere il linguaggio idoneo per la soluzione di un problema
- apprendere velocemente l'uso di un nuovo linguaggio.
Prerequisiti
Sono raccomandati corsi su Metodi Formali. Una solida esperienza di programmazione è considerata un requisito.
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 è orale e individuale.
Il voto finale è determinato da una media pesata dei punteggi ottenuti nell'esame finale, negli argomenti di approfondimento con seminario, nella partecipazione in classe, secondo la seguente partizione (indicativa e soggetta a possibili modifiche) :
30% approfondimento e seminario, 65% esame finale, 5% partecipazione (che include la regolarità della frequenza, la partecipazione attiva e il contributo alle discussioni in classe).
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) Sistemi di tipo: tipi semplici, metateoria del sottotipo, algoritmi di controllo dei tipi statico e dinamico, polimorfismo e inferenza di tipo.
2) Semantica operazionale strutturata. Strategie di valutazione "strette" e "pigre", tecniche di implementazione.
3) Tre linguaggi formali minimali:
a) Espressioni e comandi Imperativi
b) Featherweight Java, come linguaggio "core" di Java e dei linguaggi orientati agli oggetti. Tipi Generici. Prova formale di "safety". Tipi intersezione per espressioni lambda.
c) il Lambda calcolo come modello dei linguaggi funzionali. Inferenza di tipo per le funzioni. Diiverse strategie di valutazione per la chiamata delle funzioni e conseguenze. Prova formale di "safety".
4) Meccanismi di sicurezza per modellare le interazioni fra le comunicazioni in un sistema distribuito. Uso dei Tipi Sessione per descrivere protocolli di comunicazione con verifica dinamica: i protocolli sono implementati (e aggiornati) in modo da garantire che non si verifichino situazioni inattese, come un deadlock.