Semantica

Obiettivi Formativi

Scopo del corso è quello di introdurre le principali tecniche matematiche usate nello studio dei linguaggi di programmazione:

Il corso, di tipo prettamente teorico, si rivolge a studenti della laurea specialistica in informatica con forti interessi allo studio dei fondamenti dei linguaggi di programmazione.

Il corso presuppone le competenze acquisite nei corsi di "Programmazione", "Logica", "Algebra" e "Fondamenti dell'informatica" della laurea triennale in informatica.

Attività Formativa

L'attività formativa sarà basata su lezioni frontali.

Programma

  1. Il concetto di semantica dei linguaggi di programmazione: il caso di un semplicissimo linguaggio imperativo
  2. Il lamda-calcolo tipato semplice: sintassi e semantica
  3. Il linguaggio PCF (Programming Language for Computable Functions)
    1. Semantica operazionale di PCF: Call-by-Value
    2. Ordini parziali completi (CPO) e punti fissi
    3. Semantica a Punto-Fisso di PCF
    4. Confronto tra semantica operazionale e semantica denotazionale
    5. Call-by-Value per PCF
  4. Polimorfismo
    1. Il sistema polimorfo di tipi di ML
    2. Il sistema di inferenza dei tipi
    3. Il lambda-calcolo polimorfo: sistema F di Girard (cenni)