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

Article (published at ESOP'18): pdf

Source code

Git repository

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