Truly modular (co)datatypes for Isabelle/HOL

Conference paper

Blanchette, J., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A. and Traytel, D. 2014. Truly modular (co)datatypes for Isabelle/HOL. 5th International Conference on Interactive Theorem Proving (ITP). Vienna, Austria 14 - 17 Jul 2014 Springer International Publishing. pp. 93-110
TypeConference paper
TitleTruly modular (co)datatypes for Isabelle/HOL
AuthorsBlanchette, J., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A. and Traytel, D.
Abstract

We extended Isabelle/HOL with a pair of definitional commands for datatypes and codatatypes. They support mutual and nested (co)recursion through well-behaved type constructors, including mixed recursion–corecursion, and are complemented by syntaxes for introducing primitive (co)recursive functions and by a general proof method for reasoning coinductively. As a case study, we ported Isabelle’s Coinductive library to use the new commands, eliminating the need for tedious ad hoc constructions.

Research GroupFoundations of Computing group
Conference5th International Conference on Interactive Theorem Proving (ITP)
Page range93-110
ISSN0302-9743
ISBN
Hardcover9783319089690
PublisherSpringer International Publishing
Publication dates
Print14 Jul 2014
Publication process dates
Deposited23 Apr 2015
Output statusPublished
Accepted author manuscript
Copyright Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-08970-6_7

Additional information

Online ISBN: 9783319089706
Published paper appears in: Interactive Theorem Proving, Volume 8558 of the series Lecture Notes in Computer Science pp 93-110, 2014

Web address (URL)http://dx.doi.org/10.1007/978-3-319-08970-6_7
LanguageEnglish
Book titleInteractive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings
Permalink -

https://repository.mdx.ac.uk/item/8511q

Log in to edit

Download files

Accepted author manuscript
codat-impl.pdf

  • 19
    total views
  • 31
    total downloads
  • 1
    views this month
  • 2
    downloads this month

Export as