Coalgebra: abstract tools for reasoning on state-based systems
Description
Coalgebra is a branch of category theory that makes it possible to model and reason about state-based systems including concurrent and/or probabilistic programming languages, streams, automata.
In this course we will introduce several concrete and standard systems from the literature, as well as reasoning techniques on them based on equivalences and operational semantics. We will show how different state-based systems can be modelled abstractly and in a unifying way via coalgebras, and we will introduce the key concepts and theorems from order theory and category theory that make it possible to reason efficiently about such systems.
We will cover the following topics:
- Robin Milner's calculus of communicating systems (CCS)
- Probabilistic systems
- Behavioral equivalences and metrics
- Universal algebra and coalgebra
- Abstract theory of induction and coinduction
- Generalised powerset construction
- Corecursion schemes
- Computational effects as monads
Prerequisites
Familiarity with logic and operational semantics.
Basic intuitions about universal algebra and category theory would be a plus.
Teachers
Valeria Vignudelli and
Damien Pous
References
- Robin Milner, “Communication and Concurrency”, Prentice Hall.
- Bart Jacobs, “Introduction to Coalgebra”, Cambridge University Press.
- Davide Sangiorgi, “Introduction to Bisimulation and Coinduction”, Cambridge University Press.
- Yuxin Deng, "Semantics of Probabilistic Processes. An Operational Approach", Springer Berlin.
- Brian Davey and Hilary Priestley, “Introduction to Lattices and Order”, Cambridge University Press.
- Benjamin C. Pierce, “Basic Category Theory for Computer Scientists”, MIT Press.