Corso di Informatica Teorica. Anno Accademico 2003-2004.

Dipartimento di Informatica, Sistemi e Produzione. Computer Science Department.

Docente: Alberto Pettorossi. You can talk to the teacher after the lectures or by appointment.
Lectures: from 29.09.03 to 21.11.03
          Monday   16:00-17:45 (Room 10 n.e.)
          Tuesday  11:30-13:15 (Room 09 n.e.)
          Friday   11:30-11:15 (Room 10 n.e.)

Exams:    Wednesday 26.11.03  15:00   (Room 11 n.e.)
          Wednesday 03.12.03  15:00   (Room 11 n.e.)
          14.09.04   10:00  (Room 6 n.e.) Seminario didattico scientifico su argomenti di esame
          16.09.04   10:00  (Room 6 n.e.) Primo Appello (*)
          28.09.04   14:30  (Room 6 n.e.) Secondo Appello
(*)
---
(*) 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, concorrenti e a oggetti. 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 1. Fondamenti di Informatica 2.
                           Algoritmi e Strutture di Dati. Programmazione a oggetti e concorrente.
Modalità di esame: 
(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.
Esercizi e progetti debbono essere svolti dallo studente da solo.

Testi consigliati.
[Pe1] Pettorossi, A.: Quaderni di Informatica. Parte I - III, UniTor (1991), Aracne (1993).
[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
-------------------------------------------------------------

This page should be stored in:  pettorossi1:/home/adp/www/ProgramCorsoIT03-04.html