Program-ing Dependent Finger Trees in Coq

Abstract : Finger Trees (Hinze and Paterson 2006) are a general purpose persistent data structure with good performance. Their genericity permits developing a wealth of structures like ordered sequences or interval trees on top of a single implementation. However, the type systems used by current functional languages do not guarantee the coherent parameterization and specialization of Finger Trees, let alone the correctness of their implementation.We present a certified implementation of Finger Trees solving these problems using the PROGRAM extension of COQ. We not only implement the structure but also prove its invariants along the way, which permit building certified structures on top of Finger Trees in an elegant way.
Type de document :
Article dans une revue
ACM SIGPLAN Notices, Association for Computing Machinery (ACM), 2007, Proceedings of the ICFP '07 conference, 42 (9), pp.13-24. 〈10.1145/1291151.1291156〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00628867
Contributeur : Matthieu Sozeau <>
Soumis le : mardi 4 octobre 2011 - 13:59:00
Dernière modification le : mardi 24 avril 2018 - 13:38:49

Identifiants

Collections

Citation

Sozeau Matthieu. Program-ing Dependent Finger Trees in Coq. ACM SIGPLAN Notices, Association for Computing Machinery (ACM), 2007, Proceedings of the ICFP '07 conference, 42 (9), pp.13-24. 〈10.1145/1291151.1291156〉. 〈inria-00628867〉

Partager

Métriques

Consultations de la notice

54