Document Open Access Logo

Proving Tree Algorithms for Succinct Data Structures

Authors Reynald Affeldt , Jacques Garrigue , Xuanrui Qi , Kazunari Tanaka

Thumbnail PDF


  • Filesize: 0.49 MB
  • 19 pages

Document Identifiers

Author Details

Reynald Affeldt
  • National Institute of Advanced Industrial Science and Technology, Tsukuba, Japan
Jacques Garrigue
  • Graduate School of Mathematics, Nagoya University, Japan
Xuanrui Qi
  • Department of Computer Science, Tufts University, Medford, MA, United States
Kazunari Tanaka
  • Graduate School of Mathematics, Nagoya University, Japan


We acknowledge the support of the JSPS-CNRS bilateral program "FoRmal tools for IoT sEcurity" and the JSPS KAKENHI Grant Number 18H03204, thank the projects' participants, in particular Akira Tanaka for his comments on code extraction, and the anonymous reviewers for their comments that helped improve this paper.

Cite AsGet BibTex

Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka. Proving Tree Algorithms for Succinct Data Structures. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 5:1-5:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)


Succinct data structures give space-efficient representations of large amounts of data without sacrificing performance. They rely on cleverly designed data representations and algorithms. We present here the formalization in Coq/SSReflect of two different tree-based succinct representations and their accompanying algorithms. One is the Level-Order Unary Degree Sequence, which encodes the structure of a tree in breadth-first order as a sequence of bits, where access operations can be defined in terms of Rank and Select, which work in constant time for static bit sequences. The other represents dynamic bit sequences as binary balanced trees, where Rank and Select present a low logarithmic overhead compared to their static versions, and with efficient insertion and deletion. The two can be stacked to provide a dynamic representation of dictionaries for instance. While both representations are well-known, we believe this to be their first formalization and a needed step towards provably-safe implementations of big data.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Data structures design and analysis
  • Software and its engineering → Formal software verification
  • Coq
  • small-scale reflection
  • succinct data structures
  • bit vectors
  • self balancing trees


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail