====== Modelli di calcolo - Models of computation ====== **MOD 2013/14 (375AA, 9 CFU)** Lecturer: **Roberto Bruni** ([[http://www.di.unipi.it/~bruni|web]] - [[http://www.cli.di.unipi.it/~rbruni|CLI]] - [[mailto:rbruni@cli.di.unipi.it|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: {{:magistraleinformatica:mod:notes-mod-feb2014.pdf|February 2014}}. * A revised version of the lecture notes is also available as of October 2014: {{:magistraleinformatica:mod:notes-mod-october-2014.pdf|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 | {{:magistraleinformatica:mod:testo-2014-03-31.pdf|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 | {{:magistraleinformatica:mod:testo-2014-05-28.pdf|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 | {{:magistraleinformatica:mod:testo-2014-06-04.pdf|Exam}}\\ Students admitted to oral exam must contact the teacher to fix an appointment. | | | 39 | Wed 26/06 | 14:00-16:00 | A | {{:magistraleinformatica:mod:testo-2014-06-26.pdf|Exam}}\\ Students admitted to oral exam must contact the teacher to fix an appointment. | | | 40 | Wed 17/07 | 14:00-16:00 | C1 | {{:magistraleinformatica:mod:testo-2014-07-17.pdf|Exam}}\\ Students admitted to oral exam must contact the teacher to fix an appointment. | | | 41 | Thu 04/09 | 14:00-16:00 | N1 | {{:magistraleinformatica:mod:testo-2014-09-04.pdf|Exam}}\\ Students admitted to oral exam must contact the teacher to fix an appointment. | | | 42 | Fri 16/01 | 14:00-16:00 | L1 | {{:magistraleinformatica:mod:testo-2015-01-16.pdf|Exam}}\\ Students admitted to oral exam must contact the teacher to fix an appointment. | | | 43 | Fri 06/02 | 14:00-16:00 | L1 | {{:magistraleinformatica:mod:testo-2015-02-06.pdf|Exam}}\\ Students admitted to oral exam must contact the teacher to fix an appointment. | | ----