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
Il/la docente ha il dovere di vigilare affinché siano rispettate le regole di autenticità e originalità delle prove d'esame. Di conseguenza, nei casi in cui vi sia il sospetto di un comportamento irregolare, l'esame può prevedere un ulteriore approfondimento, contestuale alla prova d'esame, che potrà essere realizzato anche in modalità differente rispetto alle modalità sopra riportate.
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