# DSG seminar: Inductive-Coinductive Reasoning: Computability and Type Theory, 30.05.2018

## by Rob Stewart • May 24, 2018 • DSG Research Seminars: Logic and Programming Languages

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