Title: Coinductive Methods in Computer Science (and beyond)

Lecturer: Filippo Bonchi and Damien Pous, ENS Lyon

Period: 13 -- 24 April -- all lectures will be in Sala Seminari W

The induction principle is ubiquitous in computer science. For instance it is used to prove properties of programs involving finite data structures, such as natural numbers, lists and trees. For reasoning about concurrent programs or infinite data structures, like streams and infinite trees, one needs a dual principle -- coinduction -- which is the main topic of this course.
The relevance of coinductive reasoning has been usually associated with bisimilarity, a notion of equivalence that emerged at the end of the seventies in three different fields: non-well founded set theory, modal logics and concurrency theory. In the last years, coinductive methods has been studied in more and more areas of computer science, such as automata and type theory. Perhaps unexpectedly, applications to game theory and economy have been proposed recently.
We will introduce the coinductive definition and proof principles, several techniques to enhance coinductive proofs, and some algorithms to automatize such proofs. During the course, we will encounter examples stemming from different areas, with particular focus to automata and concurrency theory. If time allows, we will also give an overview to the theory of coalgebras, which is the abstract framework encompassing all these different examples.

Monday 13th 10-13
Motivations; Automata

Tuesday 14th 10-12
Hopcroft and Karp's algorithm; Bisimulations up-to equivalence

Wednesday 15th 10-12
Knaster and Tarski theorem; A lattice-theoretic perspective on up-to techniques

Thursday 16th 10-13
Relational Algebra; Kleene Algebra; Kleene Algebra with Test

Monday 20th 10-12
Bisimulations up-to congruence; Hopcroft and Karp up-to congruence

Tuesday 21st 10-12
Weighted Automata; Streams

Wednesday 22nd 10-12
CCS; GSOS specifications

Thursday 23rd 10-12
Algebras; Coalgebras; Bialgebras

Friday 24th 10-12
Partition Refinement algorithm (as terminal sequence)
Brzozowski's algorithm (as duality of observability and rechability)


Additional readings:

1) D. Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2012
2) D. Sangiorgi, J. Rutten. Advanced Topics in Bisimulation and Coinduction, Cambridge University Press, 2012