Succinct data structures give space-efficient representations of large amounts of data without sacrificing performance. They rely one 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.
@cite_18: 
@cite_10: Les systemes bases sur la Theorie des Types prennent une importance considerable tant pour la verification de programmes qu'en tant qu'outils permettant la preuve formelle de theoremes mettant en jeu des calculs complexes. Ces systemes necessitent aujourd'hui une grande expertise pour etre utilises efficacement. Nous developpons des constructions de haut niveau permettant d'utiliser les langages bases sur les theories des types dependants aussi simplement que les langages de programmation fonctionnels usuels, sans sacrifier pour autant la richesse des constructions disponibles dans les premiers. Nous etudions un nouveau langage permettant l'ecriture de programmes certifies en ne donnant que leur squelette algorithmique et leur specification. Le typage dans ce systeme donne lieu a la generation automatique d'obligations de preuve pouvant etre resolues a posteriori. Nous demontrons les proprietes metatheoriques essentielles du systeme, dont les preuves sont partiellement mecanisees, et detaillons son implementation dans l'assistant de preuve Coq. D'autre part, nous decrivons l'integration et l'extension d'un systeme de "Type Classes" venu d'Haskell a Coq via une simple interpretation des constructions liees aux classes dans la theorie des types sous-jacente. Nous demontrons l'utilite des classes de types dependantes pour la specification et la preuve et presentons une implementation economique et puissante d'une tactique de reecriture generalisee basee sur les classes. Nous concluons par la mise en œuvre de l'ensemble de ces contributions lors du developpement d'une bibliotheque certifiee de manipulation d'une structure de donnees complexe, les "Finger Trees".
@cite_7: We report on the design and preliminary evaluation of a short introductory course on interactive theorem proving and program verification using the Coq proof assistant, targeted at students with background in functional programming and software engineering. The course builds on concepts familiar from functional programming to develop understanding of logic and mechanized proving by means of the Curry-Howard isomorphism. A particular emphasis is made of the computational nature of decidable properties of various data structures. This approach is of practical importance, as Coq’s normalization can automatically simplify or discharge such properties, thus reducing the burden of constructing the proofs by hand. As a basis for teaching this style of mechanization, we use ’s Ssreflect extension of Coq and its associated libraries. In the course, we minimize the exposure to ad-hoc proof automation via tactics, and request that students develop proofs using only a small set of proof-building primitives that they should clearly understand. In addition to introducing logic as an application of functional programming, the topics covered by the course include: implementation of custom rewriting principles as instances of indexed type families, boolean reflection, implementation of algebraic structures and inheritance between them, and verification of imperative programs in separation logic and Hoare Type Theory.
There are now many proofs of programs that use , but we could not find much discussion trying to synthesize the new techniques put at work. used for teaching @cite_10 @cite_7 , observing benefits for clarity and maintainability, but also giving examples of custom tactics needed to prove programs. @cite_18 have shown how, in some cases, one can avoid relying on ad hoc tactics through an advanced technique involving overloading of lemmas. The techniques we describe in Sect. , while more rudimentary, are simple and efficient, yet we have not seen them described elsewhere.