Obiettivi formativi

Fornire una semantica formale di un programma significa esplicitare che cosa il programma fa (denota) utilizzando opportune strutture matematiche.
Durante il corso ci occuperemo di fornire una semantica denotazionale a costrutti di base di linguaggi di programmazione sia imperativi che funzionali.
La semantica che definiremo consisterà nell'interpretare un programma nella funzione che esso calcola fra domini di definizione dei dati. Studieremo poi il legame tra tale semantica tra domini e la semantica operazionale.
Per comprendere meglio la semantica denotazionale risulterà utile contestualizzare il linguaggio di programmazione in oggetto all'interno di una opportuna teoria dei tipi.
A tal scopo richiameremo la nozione di tipo e i suoi collegamenti con i sistemi logico-deduttivi e la programmazione funzionale, in particolare come la costruzione di un programma corretto corrisponda alla dimostrazione di un teorema matematico.
Faremo un ulteriore passo di astrazione procedendo ad enucleare la struttura essenziale per fornire una semantica denotazionale tramite lo studio della semantica categoriale.
Tempo permettendo, si accennerrà ad applicazioni della semantica categoriale alla costruzione di macchine astratte.

Programma del corso

• Semantica denotazionale con i domini per costrutti di base di un linguaggio imperativo.
• Teoria dei tipi: legami con i sistemi deduttivi logici e linguaggi di programmazione funzionali.
• Semantica denotazionale con i domini per costrutti di base di un linguaggio funzionale.
• Semantica categoriale come struttura algebrica delle semantiche denotazionali: le categorie cartesiane chiuse.
• Applicazioni della semantica categoriale alla costruzione di macchine astratte.

Testi di riferimento proposti:

Per consultazione: