Corso di Informatica Teorica. Anno Accademico 2007-2008.

Dipartimento di Informatica, Sistemi e Produzione.

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

Lectures: from 01.10.07 to 23.11.07
   Monday    16:00-17:45 (Room 10 n.e.)
   Tuesday   09:30-11:15 (Room 08 n.e.)
   Friday    11:30-13:15 (Room 10 n.e.)

 

Exams
   Thursday 06.12.07   15:00   (Room 08 n.e.) Seminario didattico-scientifico in preparazione all'esame
   Tuesday  18.12.07   15:45   (Room 16 Ingegneria Industriale. Accanto alla P­­residenza) Primo appello   (*)

  Tuesday   09.09.08   16:00   (Room 06 n.e.) Seminario didattico-scientifico in preparazione all'esame

   Thusday   11.09.08   15:30   (Room 02 n.e.) Primo appello   (*)

   Tuesday   16.09.08   15:30   (Room 02 n.e.)  Secondo appello (*)

---

(*) Contattare personalmente il docente. Non ci si puo` prenotare a entrambi gli appelli.

 

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 proprietà
dei  programmi scritti in tali linguaggi. L'approfondimento teorico verrà 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.

Previous Exam Questions

 Modalità di esame (indicazioni di massima):
(i) Voto nell'intervallo 18 - 20: Presentazione di 5 esercizi a scelta del take-home-exam + Progetto P1 + Orale.
(ii) Voto nell'intervallo 21 - 25: Presentazione di 10 esercizi a scelta del take-home-exam + Progetti P1 e P2 + Orale.
(iii) Voto nell'intervallo 26 - 30 e lode: Presentazione di 15 esercizi a scelta del take-home-exam + Progetti P1 e P2 e P3 + 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
-------------------------------------------------------------