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.

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

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)
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 -

Download files

Accepted author manuscript
  • 17
    total views
  • 17
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as