Foundational (co)datatypes and (co)recursion for higher-order logic

Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

14 Scopus citations


We describe a line of work that started in 2011 towards enriching Isabelle/HOL’s language with coinductive datatypes, which allow infinite values, and with a more expressive notion of inductive datatype than previously supported by any system based on higher-order logic. These (co)datatypes are complemented by definitional principles for (co)recursive functions and reasoning principles for (co)induction. In contrast with other systems offering codatatypes, no additional axioms or logic extensions are necessary with our approach.

Original languageEnglish
Title of host publicationFrontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings
EditorsClare Dixon, Marcelo Finger
PublisherSpringer Verlag
Number of pages19
ISBN (Print)9783319661667
StatePublished - 2017
Externally publishedYes
Event11th International Symposium on Frontiers of Combining Systems, FroCoS 2017 - Brasilia, Brazil
Duration: 27 Sep 201729 Sep 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10483 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference11th International Symposium on Frontiers of Combining Systems, FroCoS 2017


Dive into the research topics of 'Foundational (co)datatypes and (co)recursion for higher-order logic'. Together they form a unique fingerprint.

Cite this