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:

Requires the Procrastination library:

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, . should be run every time one wants to use the contents of the archive.