Foundational nonuniform (Co)datatypes for higher-order logic
- Resource Type
- Authors
- Jasmin Christian Blanchette; Fabian Meier; Andrei Popescu; Dmitriy Traytel
- Source
- LICS 2017: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science
LICS 2017: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. pp.1-12, ⟨10.1109/LICS.2017.8005071⟩
2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017
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., 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, 20/06/17 . https://doi.org/10.1109/LICS.2017.8005071
- Subject
- TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
010201 computation theory & mathematics
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
0202 electrical engineering, electronic engineering, information engineering
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
020207 software engineering
0102 computer and information sciences
02 engineering and technology
01 natural sciences
- Language
- English
International audience; Nonuniform (or " nested " or " heterogeneous ") data-types 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.