Computer Science Seminar Series

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

• Back to list