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
Type | Conference paper |
---|---|
Title | Foundational nonuniform (co)datatypes for higher-order logic |
Authors | Blanchette, 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 Group | Foundations of Computing group |
Conference | 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
Proceedings Title | Logic in Computer Science (LICS) |
ISBN | |
Hardcover | 978-1-5090-3018-7 |
Publisher | IEEE |
Publication dates | |
20 Jun 2017 | |
Publication process dates | |
Deposited | 20 Jun 2017 |
Accepted | 06 Feb 2017 |
Output status | Published |
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 |
Language | English |
Book title | Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
https://repository.mdx.ac.uk/item/870w7
Download files
18
total views3
total downloads0
views this month0
downloads this month