Indice
Modelli di calcolo - Models of computation
MOD 2013/14 (375AA, 9 CFU)
Lecturer: Roberto Bruni (web - CLI - email - phone 050 2212785 - fax 050 2212726)
Question time: Wednesday 15:00-17:00 or by appointment
Objectives
The introduction of five different computational models (imperative: IMP, functional: HOFL, processes: CCS, nominal: pi-calculus, probabilistic and stochastic: Segala automata and PEPA) together with induction principles and formal proof methods.
Course Overview
We introduce the principles of operational semantics, the principles of denotational semantics, and the techniques to relate one to the other for an imperative language and for a higher order functional language. Operational and observational semantics of two process description languages (CCS and pi-calculus) are presented. Several examples of temporal and modal logics are also discussed (HM, LTL, CTL*, mu-calculus). Finally, we consider operational nondeterministic models with discrete probabilities, and we present them from the perspective of probabilistic and stochastic automata, and of the PEPA calculus.
Textbook(s)
- Glynn Winskel, “The formal Semantics of Programming Languages”, MIT Press, 1993. Chapters: 1.3, 2, 3, 4, 5, 8, 11. “La Semantica Formale dei Linguaggi di Programmazione”, traduzione italiana a cura di Franco Turini, UTET 1999.
- Robin Milner, “Communication and Concurrency, Prentice Hall, 1989. Chapters: 1-7, 10.
- Lecture notes: February 2014.
- A revised version of the lecture notes is also available as of October 2014: October 2014 (the updated version contains several corrections as presented during the course: please consult it electronically and avoid printing it if you have already printed the previous version)
Exams
The evaluation will be based on written and oral exams. The written exam is not necessary if the mid-terms exams are evaluated positively.
In the written exam the student must demonstrate his/her knowledge of the course material and to organise an effective and correctly written reply.
During the oral exam the student must be able to demonstrate his/her knowledge of the course material and be able to discuss the reading matter thoughtfully and with propriety of expression.
Lectures
| N | Date | Time | Room | Lecture notes | Links |
|---|---|---|---|---|---|
| 1 | Mon 17/02 | 14:00-15:00 | C1 | Introduction to the course | |
| 2 | Wed 19/02 | 11:00-13:00 | A1 | Canceled | |
| 3 | Thu 20/02 | 11:00-13:00 | C1 | Canceled | |
| 4 | Mon 24/02 | 14:00-16:00 | C1 | Preliminaries Operational semantics of IMP | |
| 5 | Wed 26/02 | 11:00-13:00 | A1 | Operational semantics of IMP | |
| 6 | Thu 27/02 | 11:00-13:00 | C1 | Induction and recursion | |
| 7 | Mon 03/03 | 14:00-16:00 | C1 | Canceled | |
| 8 | Wed 05/03 | 11:00-13:00 | A1 | Induction and recursion Partial orders and fixpoints | |
| 9 | Thu 06/03 | 11:00-13:00 | C1 | Partial orders and fixpoints | |
| 10 | Mon 10/03 | 14:00-16:00 | C1 | Exercises on the operational semantics of IMP and induction | |
| 11 | Wed 12/03 | 11:00-13:00 | A1 | Partial orders and fixpoints: Immediate consequence operator Denotational semantics of IMP | |
| 12 | Thu 13/03 | 11:00-13:00 | C1 | Denotational semantics of IMP | |
| 13 | Mon 17/03 | 14:00-16:00 | C1 | Denotational semantics of IMP | |
| 14 | Wed 19/03 | 11:00-13:00 | A1 | Canceled | |
| 15 | Thu 20/03 | 11:00-13:00 | C1 | Exercises on partial orders and fixpoints and denotational semantics of IMP | |
| 16 | Mon 24/03 | 14:00-16:00 | C1 | Operational semantics of HOFL | |
| 17 | Wed 26/03 | 11:00-13:00 | A1 | Operational semantics of HOFL Domain theory | |
| 18 | Thu 27/03 | 11:00-13:00 | C1 | Exercises on the equivalence between the operational and denotational semantics of IMP and on the operational semantics of HOFL | |
| 19 | Mon 31/03 | 11:00-13:00 | A | First mid-term written exam | |
| 20 | Mon 07/04 | 14:00-16:00 | C1 | Correction of mid-term exam Domain theory | |
| 21 | Wed 09/04 | 11:00-13:00 | A1 | Denotational semantics of HOFL Equivalence between the operational and denotational semantics of HOFL | |
| 22 | Thu 10/04 | 12:00-13:00 | C1 | Equivalence between the operational and denotational semantics of HOFL | |
| 23 | Mon 14/04 | 14:00-16:00 | C1 | Exercises on the denotational semantics of HOFL and on the equivalence between the operational and denotational semantics of HOFL | |
| 24 | Wed 16/04 | 11:00-13:00 | A1 | CCS | |
| 25 | Thu 17/04 | 11:00-13:00 | C1 | CCS | |
| 26 | Mon 28/04 | 14:00-16:00 | C1 | CCS | |
| 27 | Wed 30/04 | 11:00-13:00 | A1 | CCS Temporal logic and mu-calculus | |
| 28 | Mon 05/05 | 14:00-16:00 | C1 | Temporal logic and mu-calculus | |
| 29 | Wed 07/05 | 12:00-13:00 | A1 | pi-calculus | |
| 30 | Thu 08/05 | 11:00-13:00 | C1 | pi-calculus | |
| 31 | Mon 12/05 | 14:00-16:00 | C1 | Exercises on CCS, mu-calculus and pi-calculus | |
| 32 | Wed 14/05 | 11:00-13:00 | A1 | Measure theory | |
| 33 | Thu 15/05 | 11:00-13:00 | C1 | Markov chains | |
| 34 | Mon 19/05 | 14:00-16:00 | C1 | Markov chains with actions and non-determinism | |
| 35 | Wed 21/05 | 11:00-13:00 | A1 | PEPA | |
| 36 | Thu 22/05 | 11:00-13:00 | C1 | Exercises on probabilistic systems | |
| 37 | Wed 28/05 | 11:00-13:00 | C | Second mid-term written exam Students admitted to oral exam must contact the teacher to fix an appointment. | |
| 38 | Wed 04/06 | 14:00-16:00 | C1 | Exam Students admitted to oral exam must contact the teacher to fix an appointment. | |
| 39 | Wed 26/06 | 14:00-16:00 | A | Exam Students admitted to oral exam must contact the teacher to fix an appointment. | |
| 40 | Wed 17/07 | 14:00-16:00 | C1 | Exam Students admitted to oral exam must contact the teacher to fix an appointment. | |
| 41 | Thu 04/09 | 14:00-16:00 | N1 | Exam Students admitted to oral exam must contact the teacher to fix an appointment. | |
| 42 | Fri 16/01 | 14:00-16:00 | L1 | Exam Students admitted to oral exam must contact the teacher to fix an appointment. | |
| 43 | Fri 06/02 | 14:00-16:00 | L1 | Exam Students admitted to oral exam must contact the teacher to fix an appointment. |