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.

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 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.

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.