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.
|Title of host publication||2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017|
|Publisher||Institute of Electrical and Electronics Engineers Inc.|
|Publication status||Published - 8 Aug 2017|
|Event||32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017 - Reykjavik, Iceland|
Duration: 20 Jun 2017 → 23 Jun 2017
|Conference||32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017|
|Period||20/06/17 → 23/06/17|