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: