A tentative formalization of compact data structures following [1]
[1] Gonzalo Navarro, Compact Data Structures---A Practical Approach, Cambridge University Press, 2016
- tree_traversal.v
- rank_select.v
- jacobson_rank_complexity.v
- pred_succ.v
- louds.v
- insert_delete.v
- set_clear.v
- dynamic_redblack.v
- dynamic_dependent_program.v
- dynamic_dependent_tactic.v
- Coq 8.12.1
- MathComp 1.11.0 or 1.12.0
git clone git@github.com:affeldt-aist/succinct.gitcd succinct
If the Requirements (see above) are already met, do:
coq_makefile -f _CoqProject -o Makefilemake
Or, if opam is installed, do:
opam install .
opam takes care of the dependencies.
MIT
We do not explicitly introduce any additional axioms. However, dynamic_dependent_program.v and (to a lesser
extent) dynamic_dependent_tactic.v uses the Program framework and thus implicitly depends on Coq.Logic.JMEq.JMEq_eq,
which is in turn equivalent to Streicher's Axiom K (i.e., dependent pattern matching).
- Most recent paper (arXiv version), presented at the 10th International Conference on Interactive Theorem Proving (ITP 2019)
- ITP 2019 slides
- TPP 2018 slides for LOUDS and dynamic bit vectors
- JSSST 2018 draft paper
- Earlier papers:
- "Formal Verification of the rank Algorithm for Succinct Data Structures", in 18th International Conference on Formal Engineering Methods (ICFEM 2016)
- "Safe Low-level Code Generation in Coq Using Monomorphization and Monadification", in Journal of Information Processing, vol. 26 (2018)