Informatica Teorica 2011/2012

Informazioni in: http://www.iasi.cnr.it/~adp/indexTeaching.html

Decidabilità e Computabilità di Turing. Funzioni ricorsive parziali. Induzione Strutturale, Induzione ben-fondata, rule induction. Teorema di Ricorsione. Semantica operazionale, denotazionale e assiomatica di un linguaggio imperativo. Triple di Hoare per la correttezza parziale. Calcolo di Hoare: soundness  e completezza relativa. Semantica operazionale e denotazionale di un linguaggio funzionale del primo ordine: call-by-value and call-by-name. Teoria dei domini. Un metalinguaggio per la semantica denotazionale. Teorema di Bekic.Predicati inclusivi e prove di proprietà di linguaggi funzionali. 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. Semantica operazionale e denotazionale di programmi di clausole di Horn. Comandi con guardia nondeterministici alla Dijkstra. Regole di Owicki-Gries per programmi paralleli. Calcolo di Milner per processi concorrenti comunicanti. mu-calcolo e prove di sistemi comunicanti e di protocolli. Model checking locale.