COinductive METhods in computer science - M2IF      


Filippo Bonchi Daniel Hirschkoff Damien Pous

Contents of the course

This course focuses on the usage of coinductive reasoning in computer science. Any person we meet in the street knows how to do proofs by induction over the set of natural numbers, and this proof technique can be generalised to an arbitrary inductively defined set. Coinduction is the defined as the dual of induction, and makes it possible to reason about infinite entities.
In this course, we will first introduce coinduction, the bisimulation proof method, and enhancements of bisimulation proofs.
We will then cover several fields in which coinductive reasoning can be used. These include:


The main reference for the course is
"Introduction to Bisimulation and Coinduction", by Davide Sangiorgi, Cambridge University Press.

In addition to this, links to several book chapters or research papers will be provided, in relation with the aforementioned topics (for some of these, coinductive reasoning is at a rather early stage).
You can also have a look at this paper to get some ideas about coinduction and its uses.


(Very simple) exercises will be given at each course, to be handed at the following course.