Docente
|
CENCIARELLI PIETRO
(programma)
Nozioni preliminari
– Algebra
• Induzione strutturale
• Tipi induttivi (naturali, liste, alberi...) • Sintassi astratta
– Co-algebra
• Co-induzione
• Oggetti e tipi di dato astratto Parte I: paradigmi di programmazione
– Il paradigma funzionale
• Binding statico e binding dinamico
• Valutazione lazy e valutazione eager
• Semantica di un (mini) linguaggio funzionale
– Il paradigma imperativo • Le locazioni
• Il passaggio dei parametri (valore, reference e nome)
• Semantica di un (mini) linguaggio Algol-like – Il paradigma ad oggetti (cenni)
Parte II: correttezza di programmi
– Specifica e verifica nei linguaggi imperativi • Il metodo delle invarianti
• Hoare Logic
– Specifica e verifica nei linguaggi funzionali • Teorie equazionali
• Una teoria dei tipi dipendenti
Parte III: sistemi dei tipi
– I tipi nei linguaggi funzionali
• Annotazioni di tipo come specifica • Inferenza dei tipi come verifica
– Il polimorfismo • Tipi generici
• Il polimorfismo in ML
Epilogo
– Una mappa concettuale: linguaggi, logica, algebra e modelli.
![](/images/icon-multipage.png) Dispense: http://wwwusers.di.uniroma1.it/~lpara/DISPENSE/note.pdf
|