Vous pouvez vous abonner à nos annonces de séminaires
http://gallium.inria.fr/seminaires/
S E M I N A I R E
__
/ _` _ / / o
/ ) __) / / / / / /\/|
(___/ (_/ (_ (_ / (__/ / |
I N R I A - Paris
2 rue Simone Iff (ou: 41 rue du Charolais)
Salle Lions 1, bâtiment C
Lundi 23 septembre, 10h30
----------------
Jacques Garrigue
----------------
Nagoya University
====================================================
Proving tree algorithms for succinct data structures
====================================================
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.
This is joint work with Reynald Affelt, Xuanrui Qi, and Kazunari Tanaka.