R. Affeldt, C. Cohen, and D. Rouhling, Formalization techniques for asymptotic reasoning in classical analysis, Journal of Formalized Reasoning, vol.11, issue.1, pp.43-76, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01719918

E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini, Cost analysis of object-oriented bytecode programs, Theoretical Computer Science, vol.413, issue.1, pp.142-159, 2012.

R. Atkey, Amortised resource analysis with separation logic, Logical Methods in Computer Science, vol.7, issue.2, p.17, 2011.

M. A. Bender, J. T. Fineman, S. Gilbert, and R. E. Tarjan, A new approach to incremental cycle detection and related problems, ACM Transactions on Algorithms, vol.12, issue.2, 2016.

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.

A. Charguéraud, Characteristic formulae for the verification of imperative programs, 2013.

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

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

R. Chen, C. Cohen, J. Lévy, S. Merz, and L. Théry, Formal proofs of Tarjan's algorithm in Why3, Coq, and Isabelle. Manuscript, 2018.

R. Chen and J. Lévy, A semi-automatic proof of strong connectivity, Verified Software: Theories, Tools and Experiments, vol.10712, pp.49-65, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01632947

N. Anders-danielsson, Lightweight semiformal time complexity analysis for purely functional data structures, Principles of Programming Languages (POPL), 2008.

J. Esparza, P. Lammich, R. Neumann, T. Nipkow, A. Schimpf et al., A fully verified executable LTL model checker, Computer Aided Verification (CAV), vol.8044, pp.463-478, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01226469

J. Giesl, C. Aschermann, M. Brockschmidt, F. Emmes, F. Frohn et al., Analyzing program termination and complexity automatically with AProVE, Journal of Automated Reasoning, vol.58, issue.1, pp.3-31, 2017.

S. Gulwani, SPEED: symbolic complexity bound analysis, Computer Aided Verification (CAV), vol.5643, pp.51-62, 2009.

S. Gulwani, K. K. Mehra, and T. M. Chilimbi, SPEED: precise and efficient static estimation of program computational complexity, Principles of Programming Languages (POPL), pp.127-139, 2009.

A. Guéneau, Dune pull request #1955, 2019.

A. Guéneau, A. Charguéraud, and F. Pottier, A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification, European Symposium on Programming, vol.10801, pp.533-560, 2018.

P. L. Maximilian, T. Haslbeck, and . Nipkow, Hoare logics for time bounds: A study in meta theory, Tools and Algorithms for Construction and Analysis of Systems (TACAS), vol.10805, pp.155-171, 2018.

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.

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

B. Holland, R. Ganesh, P. Santhanam, S. Awadhutkar, and . Kothari, Statically-informed dynamic analysis tools to detect algorithmic complexity vulnerabilities, Source Code Analysis and Manipulation (SCAM), pp.79-84, 2016.

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

J. Jourdan, Coq pull request #89, 2015.

R. Jung, R. Krebbers, J. Jourdan, A. Bizjak, L. Birkedal et al., Iris from the ground up: A modular foundation for higher-order concurrent separation logic, Journal of Functional Programming, vol.28, issue.20, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01945446

P. Lammich, Verified efficient implementation of Gabow's strongly connected component algorithm, Interactive Theorem Proving (ITP), vol.8558, pp.325-340, 2014.

P. Lammich, Refinement to Imperative/HOL, Interactive Theorem Proving (ITP), vol.9236, pp.253-269, 2015.

P. Lammich and R. Neumann, A framework for verifying depth-first search algorithms, Certified Programs and Proofs (CPP), pp.137-146, 2015.

C. Lemieux, R. Padhye, K. Sen, and D. Song, PerfFuzz: Automatically generating pathological inputs, International Symposium on Software Testing and Analysis (ISSTA), pp.254-265, 2018.

R. Madhavan, S. Kulal, and V. Kuncak, Contract-based resource verification for higher-order functions with memoization, Principles of Programming Languages (POPL), pp.330-343, 2017.

J. A. Mccarthy, B. Fetscher, M. S. New, D. Feltey, and R. B. Findler, A Coq library for internal verification of running-times, Functional and Logic Programming, vol.9613, pp.144-162, 2016.

R. Mudduluru and . Murali-krishna-ramanathan, Efficient flow profiling for detecting performance bugs, International Symposium on Software Testing and Analysis (ISSTA), pp.413-424, 2016.

G. Mével, J. Jourdan, and F. Pottier, Time credits and time receipts in Iris, European Symposium on Programming, vol.11423, pp.1-27, 2019.

T. Nipkow, Amortized complexity verified, Interactive Theorem Proving (ITP), vol.9236, pp.310-324, 2015.

O. Olivo, I. Dillig, and C. Lin, Static detection of asymptotic performance bugs in collection traversals, Programming Language Design and Implementation (PLDI), pp.369-378, 2015.

M. Parkinson and G. Bierman, Separation logic and abstraction, Principles of Programming Languages (POPL), pp.247-258, 2005.

F. Pottier, Depth-first search and strong connectivity in Coq, Journées Françaises des Langages Applicatifs (JFLA), 2015.
URL : https://hal.archives-ouvertes.fr/hal-01096354

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

D. M. Russinoff, A mechanically verified incremental garbage collector, Formal Aspects of Computing, vol.6, issue.4, pp.359-390, 1994.

M. Sozeau and N. Tabareau, Universe polymorphism in Coq, Interactive Theorem Proving (ITP), vol.8558, pp.499-514
URL : https://hal.archives-ouvertes.fr/hal-00974721

. Springer, , 2014.

A. Srikanth, B. Sahin, and W. R. Harris, Complexity verification using guided theorem enumeration, Principles of Programming Languages (POPL), pp.639-652, 2017.

J. Street, Dune: A composable build system, 2018.

. Robert-endre-tarjan, Amortized computational complexity. SIAM Journal on Algebraic and Discrete Methods, vol.6, issue.2, pp.306-318, 1985.

. Robert-endre-tarjan, Algorithmic design, Communications of the ACM, vol.30, issue.3, pp.204-212, 1987.

, The Coq development team. The Coq Proof Assistant, 2019.

M. Luca-della-toffola, T. R. Pradel, and . Gross, Synthesizing programs that expose performance bottlenecks, Code Generation and Optimization (CGO), pp.314-326, 2018.

J. Eelis-van-der-weegen and . Mckinna, A machine-checked proof of the average-case complexity of Quicksort in Coq, Types for Proofs and Programs, vol.5497, pp.256-271, 2008.

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