Semantica dei linguaggi di programmazione

Corso di Laurea Magistrale in Informatica


Docente

Finalità del corso

Scopo del corso è presentare la semantica formale dei linguaggi di programmazione attraverso l'uso di proof assistant. La semantica formale descrive in maniera rigorosa, non ambigua, il comportamento dei programmi. I proof assistant sono strumenti software che supportano la scrittura di prove formali, verificando la correttezza dei passaggi logici e completando autonomamente la parti più semplici delle dimostrazioni. Il corso fa ampio uso di esempi, e gran parte del corso viene presentato attraverso l'interazione con il proof assistant Coq.

Programma del CORSO

Il corso è diviso in due parti. Una prima parte di introduzione al proof assistant Coq, descrive la logica formale su cui Coq è basato e mostra, attraverso una serie di esempi, come si interagisce con esso. Nella seconda parte, Coq viene utilizzato per descrivere formalmente la semantica operazionale di alcuni semplici linguaggi di programmazione e quindi per provare la correttezza di alcuni programmi. Argomenti trattati. Programmazione funzionale in Coq: strutture dati, polimorfismo. Dimostrazioni in Coq: logica, tipi dipendenti, principi di induzione, tattiche di dimostrazione. Dimostrazioni come programmi: corrispondenza di Curry-Howard. Codifica di un linguaggio imperativo: lexer, parser, semantica operazionale. Equivalenze tra programmi, logica di Hoare. Dimostrazione di correttezza di alcuni algoritmi di ordinamento: insertion sort, merge sort, alberi binari di ricerca.

Libri di testo

Materiale presentato a lezione

Lucidi e codice Coq.

Modalità di svolgimento dell'esame

L'esame è diviso in due parti: