Corso
di Informatica Teorica. Anno Accademico
2008-2009.
Primo
anno della Laurea Specialistica in Ingegneria Informatica.
Dipartimento
di Informatica, Sistemi e Produzione.
Docente: Alberto Pettorossi. CurriculumVitae.
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.
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
-------------------------------------------------------------