Informatica Teorica 2012/2013

1. Decidabilità e Computabilità di Turing. Funzioni ricorsive parziali.

2. Induzione Strutturale, Induzione ben-fondata, rule induction. Teorema di Ricorsione.

3. Semantica operazionale, denotazionale e assiomatica di un linguaggio imperativo. Triple di Hoare per la correttezza parziale. Calcolo di Hoare: soundness  e completezza relativa.

4. Semantica operazionale e denotazionale di un linguaggio funzionale del primo ordine: call-by-value and call-by-name.

5. Teoria dei domini. Un metalinguaggio per la semantica denotazionale. Teorema di Bekic. Predicati inclusivi e prove di proprietà di linguaggi funzionali.

6. Semantica operazionale e denotazionale di un linguaggio funzionale di ordine elevato: semantica eager e semantica lazy. Operatori di punto fisso. Regole beta e eta. Adequacy e full abstraction.

7. Semantica operazionale e denotazionale di programmi di clausole di Horn.

8. Comandi con guardia nondeterministici alla Dijkstra. Regole di Owicki-Gries per programmi paralleli. Calcolo di Milner per processi concorrenti comunicanti.

9. mu-calcolo e prove di sistemi comunicanti e di protocolli. Model checking locale.