Speaker: Henning Basold, University of Lyon.

Title: Inductive-Coinductive Reasoning: Computability and Type Theory

Location: EM 1.83, 13:15, 30th May.

Abstract

Induction and coinduction are well-studied and ubiquitous principles in
both mathematics and computer science. Many interesting structures and
properties can be described inductively, coinductively or by a
combination of both. For this reason, it is beneficial to take
inductive-coinductive structures serious in logical systems that shall
be widely applicable. But there is more. Even the basic connectives of
first-order logic can be described either inductively or coinductively.
This is sort of folklore, but part of this talk is to develop a theory
that internalises this correspondence.

In this talk, we will first see the prevalence of inductive-coinductive
reasoning on the example of computability theory. In the second part, we
will explore a dependent type theory that is purely based on
inductive-coinductive types. Nonetheless, this type theory subsumes
first-order (intuitionistic) logic and primitive recursive arithmetic.
To ensure that the resulting proof system is sound, we show strong
normalisation for terms of that theory.