Armaël Guéneau

A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification

Preprint: pdf

Source code

Git repository

On Inria's gitlab: https://gitlab.inria.fr/agueneau/coq-bigO/

Requires the Procrastination library: https://gitlab.inria.fr/agueneau/coq-procrastination

Self-contained archive

The following archive bundles the library and quick setup scripts. To use it:

The 3 first steps should only be run once. Afterwards, . env.sh should be run every time one wants to use the contents of the archive.