Welcome!
Introduction
Welcome to Coinduction in Type Theory (CoTT), a workshop organised from July 3 to July 6, 2017, on the scientific campus of Le Bourget-du-Lac, France.
The term coinduction refers to a set of techniques for reasoning about infinite structures. In concurrency theory, coinduction is at the heart of the notion of bisimilarity, a very important tool for proving program equivalence. Coinduction also plays a rôle in reactive programming to model streams, and more generally in programming to represent infinite data structures. Recently, it has found effectful use in the theory of infinite dimensional categorical structures.
Proof assistants offer several alternative approaches to coinduction, from specific, built-in features as in Agda and Coq to parametric encodings à la Plotkin-Abadi, through the more recent guarded coinduction.
The workshop aims at gathering people from various approaches to coinduction, practitioners and theoreticians, and creating good conditions for dialogue. We hope to gain a clearer picture of the state of the art, and learn more about how these approaches compare with each other, in foundations as well as in applications.
The workshop will revolve around three invited mini-courses:
- Henning Basold: Type Theory Based on Dependent Inductive and Coinductive Types,
- Neil Ghani: Coinduction and infinite games,
- Rasmus Møgelberg: Guarded dependent type theory with coinductive types.
Contributed talks are solicited as well. They will be announced here as they arrive.
Registration is free, and open until June 15, but mandatory for dimensioning coffee breaks. Access to the talks is free.
