Article

Program-ing finger trees in Coq

Author:

Matthieu SozeauAuthors Info & Claims

ICFP '07: Proceedings of the 12th ACM SIGPLAN international conference on Functional programming

Pages 13 - 24

https://doi.org/10.1145/1291151.1291156

Published: 01 October 2007 Publication History

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.

References

[1]

Edwin Brady, Conor McBride, and James McKinna. Inductive families need not store their indices. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, TYPES, volume 3085 of LNCS, pages 115--129. Springer, 2003.

[2]

Adam Chlipala. Position paper: Thoughts on programming with proof assistants. In PLPV'06: Proceedings of the Programming Languages meets Program Verification Workshop, August 2006.

[3]

Coq. The Coq proof assistant. coq.inria.fr.

[4]

Thierry Coquand. Alfa/agda. In Freek Wiedijk, editor, The Seventeen Provers of the World, volume 3600 of LNCS, pages 50--54. Springer, 2006.

[5]

Jean-Christophe Filliâtre and Pierre Letouzey. Functors for proofs and programs. In David A. Schmidt, editor, ESOP, volume 2986 of LNCS, pages 370--384. Springer, 2004.

[6]

Seth Fogarty, Emir Pasalic, Jeremy Siek, and Walid Taha. Concoqtion: indexed types now! In G. Ramalingam and Eelco Visser, editors, PEPM, pages 112--121. ACM, 2007.

Digital Library

[7]

Haskell. The Haskell programming language. haskell.org.

[8]

Ralf Hinze and Ross Paterson. Finger Trees: A Simple General-purpose Data Structure. J. Funct. Program., 16(2):197--217, 2006.

Digital Library

[9]

Pierre Letouzey. A new extraction for coq. In Herman Geuvers and Freek Wiedijk, editors, TYPES'02, volume 2646 of LNCS, pages 200--219. Springer, 2002.

Digital Library

[10]

Conor McBride. Dependently Typed Functional Programs and Their Proofs. PhD thesis, University of Edinburgh, 1999.

[11]

Conor McBride and James McKinna. The view from the left. J. Funct. Program., 14(1):69--111, 2004.

Digital Library

[12]

Alexandre Miquel. The implicit calculus of constructions. In TLCA, volume 2044 of LNCS, pages 344--359. Springer, 2001.

[13]

OCaml. The Ocaml programming language. caml.inria.fr.

[14]

Sam Owre and Natarajan Shankar. The formal semantics of PVS. Technical Report SRI-CSL-97-2, Computer Science Laboratory, SRI International, Menlo Park, CA, August 1997.

[15]

Catherine Parent. Synthesizing proofs from programs in the Calculus of Inductive Constructions. In Bernhard Möller, editor, MPC, volume 947 of LNCS, pages 351--379. Springer, 1995.

Digital Library

[16]

Christine Paulin-Mohring. Inductive definitions in the system COQ. In Typed Lambda Calculi and Applications, volume 664 of LNCS, pages 328--345. Springer, 1993.

[17]

Tim Sheard. Languages of the future. SIGPLAN Notices, 39(12): 119--132, 2004.

Digital Library

[18]

Matthieu Sozeau. Subset coercions in Coq. In TYPES'06, volume 4502 of LNCS, pages 237--252. Springer, 2007.

[19]

Benjamin Werner. On the strength of proof-irrelevant type theories. 3rd International Joint Conference on Automated Reasoning, 2006.

Digital Library

[20]

Hongwei Xi. Applied Type System (extended abstract). In post-workshop Proceedings of TYPES 2003, pages 394--408. Springer-Verlag LNCS 3085, 2004.

[21]

Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), San Antonio, Texas, pages 214--227, January 1999.

Digital Library

Cited By

Sozeau MAnand ABoulier SCohen CForster YKunze FMalecha GTabareau NWinterhalter T(2020)The MetaCoq ProjectJournal of Automated Reasoning10.1007/s10817-019-09540-0Online publication date: 18-Feb-2020
https://doi.org/10.1007/s10817-019-09540-0
Sozeau MMangin C(2019)Equations reloaded: high-level dependently-typed functional programming and proving in CoqProceedings of the ACM on Programming Languages10.1145/33416903:ICFP(1-29)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341690
Winterhalter TSozeau MTabareau NMahboubi AMyreen M(2019)Eliminating reflection from type theoryProceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3293880.3294095(91-103)Online publication date: 14-Jan-2019
https://dl.acm.org/doi/10.1145/3293880.3294095
Show More Cited By

Index Terms

Program-ing finger trees in Coq
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Correctness
      2. Formal methods
2. Theory of computation
  1. Logic
    1. Proof theory
  2. Semantics and reasoning
    1. Program reasoning
      1. Program specifications
      2. Program verification

Recommendations

Finger trees explained anew, and slightly simplified (functional pearl)
Haskell 2020: Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell

We explicitly motivate the subtle intricacies of Hinze and Paterson's Finger Tree datastructure, by step-wise refining a naive implementation. The result is a new explanation of how Finger Trees work and why they have the particular structure they have, ...
Coq Coq correct! verification of type checking and erasure for Coq, in Coq

Coq is built around a well-delimited kernel that perfoms typechecking for definitions in a variant of the Calculus of Inductive Constructions (CIC). Although the metatheory of CIC is very stable and reliable, the correctness of its implementation in Coq ...
Program-ing finger trees in Coq
Proceedings of the ICFP '07 conference

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, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '07: Proceedings of the 12th ACM SIGPLAN international conference on Functional programming

October 2007

346 pages

ISBN:9781595938152

DOI:10.1145/1291151

General Chair:
Ralf Hinze
Universität Bonn, Germany
,
Program Chair:
Norman Ramsey
Harvard University, USA

ACM SIGPLAN Notices Volume 42, Issue 9
Proceedings of the ICFP '07 conference
September 2007
331 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1291220
Issue’s Table of Contents

Copyright © 2007 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 October 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICFP07

Sponsor:

ICFP07: ACM SIGPLAN International Conference on Functional Programming

October 1 - 3, 2007

Freiburg, Germany

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
399
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)0

Reflects downloads up to 30 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sozeau MAnand ABoulier SCohen CForster YKunze FMalecha GTabareau NWinterhalter T(2020)The MetaCoq ProjectJournal of Automated Reasoning10.1007/s10817-019-09540-0Online publication date: 18-Feb-2020
https://doi.org/10.1007/s10817-019-09540-0
Sozeau MMangin C(2019)Equations reloaded: high-level dependently-typed functional programming and proving in CoqProceedings of the ACM on Programming Languages10.1145/33416903:ICFP(1-29)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341690
Winterhalter TSozeau MTabareau NMahboubi AMyreen M(2019)Eliminating reflection from type theoryProceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3293880.3294095(91-103)Online publication date: 14-Jan-2019
https://dl.acm.org/doi/10.1145/3293880.3294095
Blanchette JMeier FPopescu ATraytel DAceto LIngólfsdóttir A(2017)Foundational nonuniform (co)datatypes for higher-order logicProceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3329995.3330006(1-12)Online publication date: 20-Jun-2017
https://dl.acm.org/doi/10.5555/3329995.3330006
Blanchette JMeier FPopescu ATraytel D(2017)Foundational nonuniform (Co)datatypes for higher-order logic2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS.2017.8005071(1-12)Online publication date: Jun-2017
https://doi.org/10.1109/LICS.2017.8005071
Stratulat S(2017)Mechanically certifying formula-based Noetherian induction reasoningJournal of Symbolic Computation10.1016/j.jsc.2016.07.01480:P1(209-249)Online publication date: 1-May-2017
https://dl.acm.org/doi/10.1016/j.jsc.2016.07.014
Clochard M(2014)Automatically Verified Implementation of Data Structures Based on AVL TreesVerified Software: Theories, Tools and Experiments10.1007/978-3-319-12154-3_11(167-180)Online publication date: 14-Oct-2014
https://doi.org/10.1007/978-3-319-12154-3_11
Norell U(2013)Interactive programming with dependent typesACM SIGPLAN Notices10.1145/2544174.250061048:9(1-2)Online publication date: 25-Sep-2013
https://dl.acm.org/doi/10.1145/2544174.2500610
Norell UMorrisett GUustalu T(2013)Interactive programming with dependent typesProceedings of the 18th ACM SIGPLAN international conference on Functional programming10.1145/2500365.2500610(1-2)Online publication date: 25-Sep-2013
https://dl.acm.org/doi/10.1145/2500365.2500610
Gordon CErnst MGrossman D(2013)Rely-guarantee references for refinement types over aliased mutable dataACM SIGPLAN Notices10.1145/2499370.246216048:6(73-84)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2499370.2462160
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents