Corso
di Informatica Teorica. Anno Accademico
2009-2010.
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 10.05.10 to 03.07.10
Wednesday
11:30-13:15 (Room 08 n.e.)
Thursday 16:00-17:45 (Room 08 n.e.)
Friday 09:30-11:15
(Room 08 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: ite2010_CognomeNome_Matricola
e il messaggio:
'Desidero prenotarmi per l'appello del
Giorno/Mese/Anno.
Ho svolto il
take-home-exam da solo. Cognome e Nome'
a cui 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.
Alla fine dell'esame scritto e prima dell'orale si consegni
un documento cartaceo con lo svolgimento del take-home-exam.
Per la prova orale si venga con un computer portatile ove
siamo istallati e pronti per l'esecuzione i programmi relativi
al progetto A1 (o ai progetti A1 e A2).
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 (Progetti A1 e A2).
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:
10 esercizi a scelta del take-home-exam + Progetto A1 + Scritto + Orale.
(ii) Voto nell'intervallo 21 - 25:
10 esercizi a scelta del take-home-exam + Progetti A1 e A2 + Scritto + Orale.
(iii) Voto nell'intervallo 26 - 30 e lode: tutti gli esercizi del
take-home-exam + Progetti A1 e A2 + Scritto + Orale.
Nota: gli esercizi e i progetti debbono essere fatti dallo studente da solo.
Testi
consigliati.
Pettorossi, A.: Lecture
Notes 2010
[P] Pettorossi, A.: Elements of Computability, Decidability, and
Complexity, Third Edition. Aracne, 2009.
[PL] Pettorossi, A., Proietti, M.: First Order Predicate Calculus and
Logic Programming, Second Edition, Aracne, 2005.
[Wi] Winskel, G.: The Formal Semantics of Programming Languages: An
Introduction,
The MIT Press (1993) (Also available in Italian).
Errata
Corrige
-------------------------------------------------------------