Skip to content

affeldt-aist/succinct

Repository files navigation

Compact data structures in Coq

A tentative formalization of compact data structures following [1]

[1] Gonzalo Navarro, Compact Data Structures---A Practical Approach, Cambridge University Press, 2016

Files

Requirements

  • Coq 8.12.1
  • MathComp 1.11.0 or 1.12.0

Compilation

  1. git clone git@github.com:affeldt-aist/succinct.git
  2. cd succinct

If the Requirements (see above) are already met, do:

  1. coq_makefile -f _CoqProject -o Makefile
  2. make

Or, if opam is installed, do:

  1. opam install .

opam takes care of the dependencies.

License

MIT

External Axioms

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).

Accompanying material

About

No description, website, or topics provided.

Resources

Stars

Watchers

Forks

Packages

No packages published

Contributors 4

  •  
  •  
  •  
  •  

Languages