Scheda programma d'esame
Anno accademico2017/18
PeriodoSecondo semestre

Programma non disponibile nella lingua selezionata
Learning outcomes

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 higher-order, concurrent and probabilistic features (e.g., domain theory, logical systems, well-founded 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.

Assessment criteria of knowledge

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.


  • 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 mid-terms 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.

Assessment criteria of skills

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. 

Assessment criteria of behaviors

Written and oral exam.


There are no prerequisites, but the students are expected to have some familiarity with discrete mathematics, first-order logic, context-free grammars, and code fragments in imperative and functional style.

Teaching methods

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, lambda-notation.
  • Functional programming and analysis of higher-order 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:

Other readings:

Non-attending students info

No variation.

Assessment methods

Written (two mid-term, 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' 



Additional web pages

Some teaching tools overviewed in the course are:

  • Haskell
  • CAAL
  • PseuCo
  • Google Go
  • Erlang
  • Orc
  • PEPA


Ultimo aggiornamento 26/07/2017 12:05