Program-ing finger trees in C oq
- 1 October 2007
- conference paper
- Published by Association for Computing Machinery (ACM)
- Vol. 42 (9) , 13-24
- https://doi.org/10.1145/1291151.1291156
Abstract
Finger Trees (Hinze & 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.Keywords
This publication has 11 references indexed in Scilit:
- ConcoqtionPublished by Association for Computing Machinery (ACM) ,2007
- On the Strength of Proof-Irrelevant Type TheoriesPublished by Springer Nature ,2006
- Finger trees: a simple general-purpose data structureJournal of Functional Programming, 2005
- Inductive definitions in the system Coq rules and propertiesPublished by Springer Nature ,2005
- Languages of the futureACM SIGPLAN Notices, 2004
- The view from the leftJournal of Functional Programming, 2004
- Inductive Families Need Not Store Their IndicesPublished by Springer Nature ,2004
- Functors for Proofs and ProgramsPublished by Springer Nature ,2004
- A New Extraction for CoqPublished by Springer Nature ,2003
- Synthesizing proofs from programs in the Calculus of Inductive ConstructionsPublished by Springer Nature ,1995