Foundational nonuniform (Co)datatypes for higher-order logic

Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

1 Downloads (Pure)


Nonuniform (or 'nested' or 'heterogeneous') datatypes are recursively defined types in which the type arguments vary recursively. They arise in the implementation of finger trees and other efficient functional data structures. We show how to reduce a large class of nonuniform datatypes and codatatypes to uniform types in higher-order logic. We programmed this reduction in the Isabelle/HOL proof assistant, thereby enriching its specification language. Moreover, we derive (co)induction and (co)recursion principles based on a weak variant of parametricity.

Original languageEnglish
Title of host publication2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Subtitle of host publication[Proceedings]
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages12
ISBN (Electronic)9781509030187
ISBN (Print)9781509030194
Publication statusPublished - 2017
Event32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017 - Reykjavik, Iceland
Duration: 20 Jun 201723 Jun 2017


Conference32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017


Acknowledgment: We thank David Basin for supporting this research, Peter Lammich for pointing us to his work on finger trees and for formalizing Okasaki’s construction for powerlists, Johannes Hölzl for taking the time to explain Lean’s nonuniform datatypes, and Mark Summerfield and the anonymous reviewers for suggesting textual improvements. Blanchette has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Popescu has received funding from UK’s Engineering and Physical Sciences Research Council (EPSRC) via the grant EP/N019547/1, Verification of Web Services (VOWS). The authors are listed alphabetically.

FundersFunder number
European Research Council
European Union’s Horizon 2020
Horizon 2020 Framework Programme713999
Engineering and Physical Sciences Research CouncilEP/N019547/1


    Dive into the research topics of 'Foundational nonuniform (Co)datatypes for higher-order logic'. Together they form a unique fingerprint.

    Cite this