Strumenti Utente

Strumenti Sito


magistraleinformatica:mod:2013-14:start

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.

magistraleinformatica/mod/2013-14/start.txt · Ultima modifica: 06/05/2015 alle 18:39 (3 anni fa) da Roberto Bruni