Corso di Informatica Teorica. Anno Accademico 2008-2009.

Primo anno della Laurea Specialistica in Ingegneria Informatica.
Dipartimento di Informatica, Sistemi e Produzione.

Docente: Alberto PettorossiCurriculumVitae.
You can talk to the teacher after the lectures or by appointment. 

Lectures: from 04.05.09 to 27.06.09
               Tuesday           14:00-15:45 (Room 11 n.e.)
               Wednesday    14:00-15:45 (Room 11 n.e.)
               Thursday        09:30-11:15 (Room 11 n.e.)

 

Exams and Seminars.
   Same time and place as the exams of the course: Automi, Linguaggi e Traduttori.

Per la prenotazione agli esami inviare al docente (pettorossi@info.uniroma2.it)
 
sette giorni prima dell'appello un email con il subject:
 
ite2009_CognomeNome_Matricola e il messaggio:
 
''Desidero prenotarmi per l'appello del Giorno/Mese/Anno.
  
Ho svolto il take-home exam da solo. CognomeNome''.
 
All'email deve essere allegato (in formato .pdf) lo svolgimento del take-home-exam.

Di norma non ci si puo' iscrivere a piu' di un appello per sessione d'esame
e non ci si puo' iscrivere a piu' di tre appelli per anno accademico.

Obiettivo del corso. Il corso si propone di offrire una panoramica dei metodi
per la definizione della semantica dei linguaggi di programmazione imperativi,
funzionali, logici e concorrenti. Tali metodi  consentono di approfondire la comprensione
logica e algebrica delle varie tecniche esistenti per la specifica e la verifica di proprieta'
dei  programmi scritti in tali linguaggi. L'approfondimento teorico verra' consolidato
dall'uso e dallo sviluppo di strumenti software opportuni.

Programma d'esame con informazioni bibliografiche.
Take-home exam.
Programma del corso:
1. Decidability and Turing computability. Partial Recursive Functions.
2. Structural induction, well-founded induction, and rule induction. Recursion Theorem.
3. Operational, denotational, and axiomatic semantics of an imperative language.
   
Hoare's triples for partial correctness. Hoare's calculus: soundness and relative completeness.
4. Operational and denotational semantics of a first order functional language:
   
call-by-value and call-by-name regimes.
5. Domain theory. A metalanguage for denotational semantics. Bekic's Theorem.
   
Inclusive predicates and proofs of properties of functional programs.
6. Operational and denotational semantics of a higher order functional language: eager semantics
   
and lazy semantics. Fixpoint operators. Beta and eta rules. Adequacy and full abstraction.
7. Operational and denotational semantics of Horn-clause programs.
8. Dijkstra's nondeterministic guarded commands. Owicki-Gries rules for parallel commands.
    
Milner's calculus for communicating concurrent processes.
9. mu-calculus and proofs of communicating systems and protocols. Local model-checking.

Prerequisiti: Fondamenti di Informatica.  Algoritmi e Strutture di Dati.
                  
Programmazione orientata agli oggetti oppure Programmazione a oggetti e concorrente.

La frequenza e' obbligatoria.

Previous Exam Questions

Handouts: Semantics of Higher Order Typed Languages

Dati statistici relativi alle votazioni d'esame conseguite dagli studenti

 Modalita' di esame (indicazioni di massima):
(i) Voto nell'intervallo 18 - 20: Presentazione di 5 esercizi a scelta del take-home-exam + Progetti P1 e P2 + Scritto + Orale.
(ii) Voto nell'intervallo 21 - 25: Presentazione di 10 esercizi a scelta del take-home-exam + Progetti P1 e P2 e P3 + Scritto + Orale.
(iii) Voto nell'intervallo 26 - 30 e lode: Presentazione di tutti gli esercizi del take-home-exam + Progetti P1 e P2 e P3 + Scritto + Orale.
Nota: gli esercizi e i progetti debbono essere fatti dallo studente da solo.

Testi consigliati.
[P] Pettorossi, A.: Elements of Computability, Decidability, and Complexity, Second Edition. Aracne, 2007.
[PL] Pettorossi, A., Proietti, M.: First Order Predicate Calculus and Logic Programming, Aracne, 2002.
[Wi]  Winskel, G.: The Formal Semantics of Programming Languages: An Introduction,
The MIT Press (1993) (Also available in Italian).
Errata Corrige
-------------------------------------------------------------