Corso di Informatica Teorica. Anno Accademico 2002-2003.

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

Docente: Alberto Pettorossi.
Tuesday       11:30-13:15 (Room 12)
Wednesday  10:30-12:15 (Room 12)
Friday            09:30-11:15 (Room 12)
Lectures: from 10.12.02 to 14.02.03.
Exams: 20.02.03  10:00 am (Room 10)
You can talk to the teacher after the lectures or by appointment.

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.

Esami: martedi` 09.09.03 ore 10 aula 12. ***
               martedi` 23.09.03 ore 10 aula 12. ***
*** Occorre fare la prenotazione nel foglio predisposto all'ingresso di Ingegneria dell'Informazione.

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:  Presentazione di un programma per la definizione della semantica
operazionale oppure per la verifica di correttezza di protocolli. Prova scritta e orale.

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/ProgramCorsoIT02-03.html