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

Conference paper

Biendarra, J., Blanchette, J., Bouzy, A., Desharnais, M., Fleury, M., Hölzl, J., Kunčar, O., Lochbihler, A., Meier, F., Panny, L., Popescu, A., Sternagel, C., Thiemann, R. and Traytel, D. 2017. Foundational (co)datatypes and (co)recursion for higher-order logic. 11th International Symposium on Frontiers of Combining Systems, FroCoS 2017. Brasilia, Brazil 27 - 29 Sep 2017 Cham Springer International Publishing. pp. 3-21 https://doi.org/10.1007/978-3-319-66167-4_1
TypeConference paper
TitleFoundational (co)datatypes and (co)recursion for higher-order logic
AuthorsBiendarra, J., Blanchette, J., Bouzy, A., Desharnais, M., Fleury, M., Hölzl, J., Kunčar, O., Lochbihler, A., Meier, F., Panny, L., Popescu, A., Sternagel, C., Thiemann, R. and Traytel, D.
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.

Conference11th International Symposium on Frontiers of Combining Systems, FroCoS 2017
Page range3-21
ISSN0302-9743
ISBN
Hardcover9783319661667
PublisherSpringer International Publishing
Place of publicationCham
Publication dates
Online29 Aug 2017
Print29 Sep 2017
Publication process dates
Deposited22 Jan 2018
Accepted06 May 2017
Output statusPublished
Accepted author manuscript
Copyright Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-66167-4_1

Additional information

Cite this paper as:
Biendarra J. et al. (2017) Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. In: Dixon C., Finger M. (eds) Frontiers of Combining Systems. FroCoS 2017. Lecture Notes in Computer Science, vol 10483. Springer, Cham

Digital Object Identifier (DOI)https://doi.org/10.1007/978-3-319-66167-4_1
LanguageEnglish
Book titleFrontiers of Combining Systems: 11th International Symposium, FroCoS 2017, Brasília, Brazil, September 27-29, 2017, Proceedings
Permalink -

https://repository.mdx.ac.uk/item/8768y

Log in to edit

Download files

Accepted author manuscript
co_data_invited.pdf

  • 10
    total views
  • 1
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as