Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic

Julian Biendarra, Jasmin 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

Proceedings of the 14th International Symposium on Frontiers of Combining Systems, LNCS 10483, pp. 3-21, 2017.


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


  PDF |    doi:10.1007/978-3-319-66167-4_1  


author = "Julian Biendarra and Jasmin Blanchette and Aymeric Bouzy and Martin Desharnais and
Mathias Fleury and Johannes Hölzl and Ondřej Kunčar and Andreas Lochbihler and
Fabian Meier and Lorenz Panny and Andrei Popescu and Christian Sternagel and
René Thiemann and Dmitriy Traytel",
title = "Foundational (Co)datatypes and (Co)recursion for
Higher-Order Logic",
booktitle = "Proceedings of the 14th International Symposium on
Frontiers of Combining Systems (FroCoS'17)",
editor = "Dixon C. and Finger M.",
series = "Lecture Notes in Computer Science",
volume = 10483,
pages = "3--31",
year = 2017,
doi = "10.1007/978-3-319-66167-4_1"
Nach oben scrollen