Un'attenta analisi dell'attività di sintesi dei programmi evidenzia un fatto fondamentale: la costruzione di un programma corretto è un attività analoga alla dimostrazione di un teorema matematico. In altre parole, con l'uso di opportuni strumenti logico-matematici, si è scoperto che la sintesi di un programma che soddisfa le specifiche di un problema dato corrisponde esattamente alla dimostrazione matematica di un particolare teorema. Pertanto è possibile servirsi della logica matematica per meglio comprendere l'attività di programmazione e, possibilmente, per creare ausilii alla programmazione corretta. Di più, una volta che l'attività di programmazione sia stata ambientata in questo contesto, è possibile usare matematica e logica per produrre modelli adeguati all'analisi della semantica dei programmi.
Nel corso si vogliono studiare approfonditamente i rapporti che intercorrono tra algoritmi, tipi, logica e modelli. Dopo aver illustrato gli argomenti classici, si affronteranno temi più avanzati orientati verso la concorrenza.
Programma del corso:
Testo di riferimento proposto: J.Y. Girard Proofs and Types Cambridge Tracts in Computer Science Cambridge University Press, 1998