FOUNDATIONS OF PROGRAMMING LANGUAGES IN COQ
- Anno accademico
- 2025/2026 Programmi anni precedenti
- Titolo corso in inglese
- FOUNDATIONS OF PROGRAMMING LANGUAGES IN COQ
- Codice insegnamento
- PHD226 (AF:588775 AR:333343)
- Lingua di insegnamento
- Inglese
- Modalità
- In presenza
- Crediti formativi universitari
- 2
- Livello laurea
- Corso di Dottorato (D.M.226/2021)
- Settore scientifico disciplinare
- INF/01
- Periodo
- Annuale
- Anno corso
- 1
- Sede
- VENEZIA
- Spazio Moodle
- Link allo spazio del corso
Inquadramento dell'insegnamento nel percorso del corso di studio
I metodi formali sono di fondamentale importanza per un informatico e questo corso di dottorato ambisce a fornire un'introduzione alla teoria dei linguaggi di programmazione.
In particolare, gli obbiettivi del corso sono: introdurre le studentesse/gli studenti alla sintassi e alla semantica dei linguaggi di programmazione in Rocq (un proof assistant precedentemente noto come Coq).
In particolare, gli obbiettivi del corso sono: introdurre le studentesse/gli studenti alla sintassi e alla semantica dei linguaggi di programmazione in Rocq (un proof assistant precedentemente noto come Coq).
Risultati di apprendimento attesi
La frequenza e la partecipazione attiva al corso e lo studio individuale consentiranno ai partecipanti di:
1. Conoscenza e comprensione
1.1. acquisire i fondamenti della sintassi e semantica dei linguaggi di programmazione in Rocq;
2. Capacità di applicare conoscenza e comprensione
2.1. sapere modellare un semplice linguaggio in Rocq;
2.2. sapere formalizzare Rocq per dimostrare semplici proprietà dei linguaggi e dei programmi.
3. Capacità di giudizio
3.1. sapere valutare le alternative formulazioni di correttezza e sicurezza dei compilatori, discutendone pregi e difetti
1. Conoscenza e comprensione
1.1. acquisire i fondamenti della sintassi e semantica dei linguaggi di programmazione in Rocq;
2. Capacità di applicare conoscenza e comprensione
2.1. sapere modellare un semplice linguaggio in Rocq;
2.2. sapere formalizzare Rocq per dimostrare semplici proprietà dei linguaggi e dei programmi.
3. Capacità di giudizio
3.1. sapere valutare le alternative formulazioni di correttezza e sicurezza dei compilatori, discutendone pregi e difetti
Prerequisiti
Gli studenti/le studentesse devono possedere una conoscenza di base della teoria degli insiemi, della logica e dell'induzione matematica. E' suggerita familiarità con almeno un linguaggio di programmazione funzionale (ad esempio, OCaml, Haskell, Agda, F#, Scala, Lean, ...).
Contenuti
* Blocco 1 (1h + 3h laboratorio)
+ Introduzione al software verificato e motivazioni
+ (Laboratorio guidato) Fondamenti di Rocq
+ (Laboratorio) Q&A su Rocq; Esercizi
* Blocco 2 (4h + 2h laboratorio)
+ Sintassi e semantica dei linguaggi di programmazione
+ Esempi: imperativo, funzionale e a basso livello
+ (Laboratorio guidato) Definizione di semplici linguaggi di programmazione, vari paradigmi di linguaggi e stili di semantica
+ Introduzione al software verificato e motivazioni
+ (Laboratorio guidato) Fondamenti di Rocq
+ (Laboratorio) Q&A su Rocq; Esercizi
* Blocco 2 (4h + 2h laboratorio)
+ Sintassi e semantica dei linguaggi di programmazione
+ Esempi: imperativo, funzionale e a basso livello
+ (Laboratorio guidato) Definizione di semplici linguaggi di programmazione, vari paradigmi di linguaggi e stili di semantica
Testi di riferimento
[1] B. C. Pierce et al., "Software foundations, Vol 1: Logical Foundations", https://softwarefoundations.cis.upenn.edu/lf-current/index.html
[2] B. C. Pierce et al., "Software foundations, Vol 2: Programming Language Foundations", https://softwarefoundations.cis.upenn.edu/plf-current/index.html
[2] B. C. Pierce et al., "Software foundations, Vol 2: Programming Language Foundations", https://softwarefoundations.cis.upenn.edu/plf-current/index.html
Modalità di verifica dell'apprendimento
Due opzioni, con un carico di lavoro previsto di circa 4/8 ore, entrambe da discutere con l'insegnante:
* Seminario: organizzare un seminario di 45 minuti/1 ora su un argomento avanzato a scelta
* Progetto: sviluppare un'estensione non banale a uno degli esercizi/argomenti trattati nel corso (ad esempio, funzionalità aggiuntive su un compilatore)
* Seminario: organizzare un seminario di 45 minuti/1 ora su un argomento avanzato a scelta
* Progetto: sviluppare un'estensione non banale a uno degli esercizi/argomenti trattati nel corso (ad esempio, funzionalità aggiuntive su un compilatore)
Modalità di esame
orale
Graduazione dei voti
L'esito dell'esame può essere: "approvato" oppure "non approvato". L'esito è "approvato" richiede:
- conoscenza sufficiente degli argomenti del programma e capacità di comprensione applicata adeguata;
- capacità autonome e coerenti di analisi, valutazione e interpretazione;
- uso appropriato e controllato della terminologia tecnica;
- esposizione chiara e ordinata.
- conoscenza sufficiente degli argomenti del programma e capacità di comprensione applicata adeguata;
- capacità autonome e coerenti di analisi, valutazione e interpretazione;
- uso appropriato e controllato della terminologia tecnica;
- esposizione chiara e ordinata.
Metodi didattici
Corso frontale che si avvale anche di esercizi svolti durante le ore di laboratorio (eventualmente online) per consolidare i concetti e favorire la discussione tra gli studenti/studentesse.
Programma definitivo.
Data ultima modifica programma: 17/11/2025