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:
automata
concurrent processes (process calculi such as CCS or the
pi-calculus)
coinductive datatypes, streams
probabilistic (quantitative) coinduction, metrics
coinductive methods for contextual equivalences (higher-order
languages, Howe's method)
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.
Exercises
(Very simple) exercises will be given at each course, to be handed at
the following course.