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.

 pdf  doi:10.1007/978-3-319-66167-4_1

Abstract

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.

BibTex

@inproceedings{JBJBABMDMFJHOKALFMLPAPCSRTDT-FroCoS17,
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"
}