Z. Z_filtertype and . Le,

. Post-(fun-y-?-uf-d-r-v,

M. A. Akra and L. Bazzi, On the solution of linear recurrence equations, Comp. Opt. and Appl, vol.10, issue.2, pp.195-210, 1998.

R. Atkey, Amortised resource analysis with separation logic, Logical Methods in Computer Science, vol.7, issue.2, p.17, 2011.
DOI : 10.2168/lmcs-7(2:17)2011

URL : https://lmcs.episciences.org/685/pdf

J. Avigad and K. Donnelly, Formalizing O notation in Isabelle/HOL, International Joint Conference on Automated Reasoning, vol.3097, pp.357-371, 2004.
DOI : 10.1007/978-3-540-25984-8_27

URL : http://www.andrew.cmu.edu/~avigad/Papers/bigo.pdf

S. Boldo, F. Clément, J. C. Filliâtre, M. Mayero, G. Melquiond et al., Wave equation numerical resolution: a comprehensive mechanized proof of a C program, Journal of Automated Reasoning, vol.50, issue.4, pp.423-456, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00649240

S. Boldo, C. Lelay, and G. Melquiond, Coquelicot: A user-friendly library of real analysis for Coq, Mathematics in Computer Science, vol.9, issue.1, pp.41-62, 2015.
URL : https://hal.archives-ouvertes.fr/hal-00860648

N. Bourbaki, General Topology, 1995.

G. Brassard and P. Bratley, Fundamentals of algorithmics, 1996.

Q. Carbonneaux, J. Hoffmann, T. Reps, and Z. Shao, Automated resource analysis with Coq proof objects, Computer Aided Verification (CAV), vol.10427, pp.64-85, 2017.
DOI : 10.1007/978-3-319-63390-9_4

A. Charguéraud, Characteristic formulae for the verification of imperative programs, International Conference on Functional Programming (ICFP), pp.418-430, 2011.

A. Charguéraud, The CFML tool and library, 2016.

A. Charguéraud and F. Pottier, Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits, Journal of Automated Reasoning, 2017.

T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein, Introduction to Algorithms, 2009.

M. Eberl, Proving divide and conquer complexities in Isabelle/HOL, Journal of Automated Reasoning, vol.58, issue.4, pp.483-508, 2017.
DOI : 10.1007/s10817-016-9378-0

J. C. Filliâtre and P. Letouzey, Functors for proofs and programs, European Symposium on Programming (ESOP), vol.2986, pp.370-384, 2004.

R. L. Graham, D. E. Knuth, and O. Patashnik, Concrete mathematics: a foundation for computer science, 1994.

A. Guéneau, A. Charguéraud, and F. Pottier, Electronic appendix, 2018.

J. Hoffmann, A. Das, and S. Weng, Towards automatic resource bound analysis for OCaml, Principles of Programming Languages (POPL), pp.359-373, 2017.
DOI : 10.1145/3093333.3009842

URL : http://dl.acm.org/ft_gateway.cfm?id=3009842&type=pdf

J. E. Hopcroft, Computer science: the emergence of a discipline, Communications of the ACM, vol.30, issue.3, pp.198-202, 1987.

R. R. Howell, On asymptotic notation with multiple variables, 2008.

R. R. Howell, Algorithms: A top-down approach, 2012.

T. Leighton, Notes on better master theorems for divide-and-conquer recurrences, 1996.

A. Pilkiewicz and F. Pottier, The essence of monotonic state, Types in Language Design and Implementation (TLDI), 2011.
DOI : 10.1145/1929553.1929565

URL : https://hal.archives-ouvertes.fr/hal-01081193

J. C. Reynolds, Separation logic: A logic for shared mutable data structures, Logic in Computer Science (LICS), pp.55-74, 2002.
DOI : 10.1109/lics.2002.1029817

URL : http://ttic.uchicago.edu/~dreyer/seplogic.pdf

R. E. Tarjan, Algorithm design, Communications of the ACM, vol.30, issue.3, pp.204-212, 1987.

P. Wang, D. Wang, and A. Chlipala, TiML: A functional language for practical complexity analysis with invariants, Proceedings of the ACM on Programming Languages, vol.1, issue.26, pp.1-79, 2017.

B. Wegbreit, Mechanical program analysis, Communications of the ACM, vol.18, issue.9, pp.528-539, 1975.
DOI : 10.1145/361002.361016