Foundational nonuniform (Co)datatypes for higher-order logic

Abstract : 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.
Type de document :
Communication dans un congrès
LICS 2017: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. pp.1 - 12, 2017, 〈10.1109/LICS.2017.8005071〉
Liste complète des métadonnées

Littérature citée [42 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01599174
Contributeur : Jasmin Christian Blanchette <>
Soumis le : dimanche 1 octobre 2017 - 18:53:00
Dernière modification le : mardi 3 octobre 2017 - 01:28:26

Fichier

conf.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, Dmitriy Traytel. Foundational nonuniform (Co)datatypes for higher-order logic. LICS 2017: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2017, Reykjavik, Iceland. pp.1 - 12, 2017, 〈10.1109/LICS.2017.8005071〉. 〈hal-01599174〉

Partager

Métriques

Consultations de
la notice

49

Téléchargements du document

4