This library is described in the paper "A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification" (at ESOP'18: preprint).
Installation instructions (using opam and the opam coq repository):
- Install Coq >= 8.6
- Install TLC, CFML, and Procrastination:
opam install coq-tlc coq-cfml coq-procrastination - Run
maketo compile the library - Run
make examplesto compile the examples