## Inductive-Coinductive Reasoning: Computability and Type Theory

**Henning Basold**

University of Lyon, France

Webpage

**Joint Computer Science / DSG Seminar**

**30 May 2018**

**1:15pm - 2:15pm**

**EM 1.83**

### 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.

**Hosts:**
Katya
Komendantskaya and
Rob Stewart