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

Abstract

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 2017
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781509030187
DOIs
Publication statusPublished - 8 Aug 2017
Event32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017 - Reykjavik, Iceland
Duration: 20 Jun 201723 Jun 2017

Conference

Conference32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017
CountryIceland
CityReykjavik
Period20/06/1723/06/17

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

  • Cite this

    Blanchette, J. C., Meier, F., Popescu, A., & Traytel, D. (2017). Foundational nonuniform (Co)datatypes for higher-order logic. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017 [8005071] Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/LICS.2017.8005071