Foundational nonuniform (co)datatypes for higher-order logic

Conference paper


Blanchette, J., Meier, F., Popescu, A. and Traytel, D. 2017. Foundational nonuniform (co)datatypes for higher-order logic. 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Reykjavik, Iceland 20 - 23 Jun 2017 IEEE. https://doi.org/10.1109/LICS.2017.8005071
TypeConference paper
TitleFoundational nonuniform (co)datatypes for higher-order logic
AuthorsBlanchette, J., Meier, F., Popescu, A. and Traytel, D.
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)recusion and (co)induction principles based on a weak variant of parametricity.

Research GroupFoundations of Computing group
LanguageEnglish
Conference32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Proceedings TitleLogic in Computer Science (LICS)
ISBN
Hardcover978-1-5090-3018-7
PublisherIEEE
Publication dates
Print20 Jun 2017
Publication process dates
Deposited20 Jun 2017
Accepted06 Feb 2017
Output statusPublished
Accepted author manuscript
Copyright Statement

© 2017 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.

Digital Object Identifier (DOI)https://doi.org/10.1109/LICS.2017.8005071
Book titleProceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Permalink -

https://repository.mdx.ac.uk/item/870w7

Download files


Accepted author manuscript
  • 16
    total views
  • 0
    total downloads
  • 2
    views this month
  • 0
    downloads this month

Export as