A tentative formalization of compact data structures following [1]
[1] Gonzalo Navarro, Compact Data Structures---A Practical Approach, Cambridge University Press, 2016
- compact_data_structures.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_makefile -f _CoqProject -o Makefilemake
- Coq 8.9.1
- MathComp 1.9.0
- Most recent draft paper (arXiv version)
- TPP 2018 slides for LOUDS and dynamic bit vectors
- JSSST 2018 draft paper