Semantica dei linguaggi di programmazione
Corso di Laurea Magistrale in Informatica
Docente
Finalità del corso
Scopo del corso è presentare la semantica dei linguaggi di programmazione attraverso l'uso di proof assistant, ossia strumenti software che aiutano la scrittura di prove formali, verificando la correttezza dei passaggi logici, e completando automaticamente la parti più semplici della dimostrazione.
Il corso è diviso in due parti, una prima parte di presentazione del proof assistant Coq, descrivendo la logica formale su cui è basato e mostrando in pratica come viene utilizzato.
Nella seconda parte, Coq viene utilizzato per descrivere formalmente la semantica operazionale e denotazionale di alcuni semplici linguaggi di programmazione e quindi per provare la correttezza di alcuni programmi esempio.
Libri di testo
Materiale presentato a lezione
Lucidi e codice Coq.
Modalità di svolgimento dell'esame
L'esame è diviso in più parti:
-
presentazione delle soluzioni degli esercizi assegnati durante l'anno;
-
presentazione di un progetto;
-
prova orale.