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

    by  • 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.


    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.