Objectives
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) is also presented. Finally, we consider operational nondeterministic models with discrete probabilities, and we present them from the perspective of probabilistic automata.

Syllabus
1) Operational and denotational semantics of a simple imperative language (IMP)
a. Introduction and proof systems based on inference rules
b. Syntax and operational semantics of IMP
c. Induction principles
d. Complete partial orderings
e. Minimal fixpoint theorem
f. Signatures and term algebras
g. Denotational semantics of IMP
h. Equivalence between operational and denotational semantics
2) Operational and denotational semantics of a higher order functional language (HOL)
a. Syntax and lazy operational semantics of HOL
b. Domains and domain constructions
c. Lazy denotational semantics of HOL
d. Relations between operational and denotational semantics of HOL
3) Transition systems and process calculi for mobile, probabilistic communicating systems
a. Syntax and operational semantics of a process calculus (CCS)
b. Observational semantics of CCS
c. Hennessy-Milner logic
d. Syntax and semantics of a process calculus for mobile systems (pi-calculus)
e. Operational models with discrete probabilities, Markov processes
f. Probabilistic automata (PA)
g. Simulation and bisimulation of PA

Course structure
9 credits (4 on IMP, 2 on HOL and 3 on process calculi). The final exam consists in written and oral parts. The written part can be replaced by two written exams taken during the course.