(COMPUTATIONAL MODELS)
CdSINFORMATICA
Codice375AA
CFU9
PeriodoSecondo semestre
LinguaInglese
Moduli  Settore/i  Tipo  Ore  Docente/i  
MODELLI DI CALCOLO  INF/01  LEZIONI  72 

Students are expected to acquire solid knowledge about concepts and techniques in the study of advanced programming languages and their formal logical underpinnings. The course will cover the basic techniques for assigning meaning to programs with higherorder, concurrent and probabilistic features (e.g., domain theory, logical systems, wellfounded induction, structural recursion, labelled transition systems, Markov chains, probabilistic reactive systems, stochastic process algebras) and for proving their fundamental properties, such as termination, normalisation, determinacy, behavioural equivalence and logical equivalence. Temporal and modal logics will also be studied for the specification and analysis of programs. In particular, some emphasis will be posed on modularity and compositionality, in the sense of guaranteeing some property of the whole by proving simpler properties of its parts.
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.
Methods:
 Final oral exam
 Final written exam
 Periodic written tests
Further information:
The evaluation will be based on written and oral exams. The written exam is not necessary if the midterms exams are evaluated positively.
At the end of the course the student should be able to state and prove formal properties of declarative, concurrent and probabilistic programs. In particular, they should be able to apply several induction principles and fixpoint theory.
The written exam consists of exercises that require to apply formal analysis techniques to some carefully chosen cases.
The oral exam focuses on the definitions and properties presented in the course.
At the end of the course the student should be able to understand logic systems and inductive definitions, to assign semantics to programs, to reason about program equivalence and compliance to abstract specifications.
Written and oral exam.
There are no prerequisites, but the students are expected to have some familiarity with discrete mathematics, firstorder logic, contextfree grammars, and code fragments in imperative and functional style.
Delivery: face to face
Learning activities:
 attending lectures
 participation in discussions
 home assignments, to be solved together in the next lecture
 individual study
Attendance: Advised
Teaching methods:
 Lectures
 Induction and recursion, partial orders, fixed points, lambdanotation.
 Functional programming and analysis of higherorder functional languages.
 Concurrent programming and analysis of concurrent and nondeterministic systems.
 Code orchestration and analysis of coordination languages.
 Models and analysis of probabilistic and stochastic systems.
Main text:
 Roberto Bruni, Ugo Montanari, “Models of Computation”, Springer Texts in Computer Science, 2017.
Other readings:
 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: 17, 10.
No variation.
Written (two midterm, or one regular) exam and oral exam.
The written exam consists of a series of exercises to be solved in 2 hours. Each exercise is assigned some score and the overal score is the sum of scores for each exercise. The texts of exams from previous sessions and academic years are linked from the web page of the course.
The oral exam can involve the discussion of the written exam as well as questions about the main topics of the course topics. The average duration of the oral exam is 40'
Some teaching tools overviewed in the course are:
 Haskell https://www.haskell.org/
 CAAL http://caal.cs.aau.dk/
 PseuCo http://pseuco.com/
 TAPAS http://rap.dsi.unifi.it/tapas/en/index.htm
 Google Go http://golang.org/
 Erlang http://www.erlang.org/
 Orc https://orc.csres.utexas.edu/
 PEPA http://www.dcs.ed.ac.uk/pepa/
None