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 TraytelProceedings of the 14th International Symposium on Frontiers of Combining Systems, LNCS 10483, pp. 3-21, 2017.
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"
}