A. Aho, J. Hopcroft, J. Ullman, M. Thorup, I. Gørtz et al., The Design and Analysis of Computer Algorithms Union-find with constant time deletions, ACM Transactions on Algorithms, vol.116, issue.1, pp.1-628, 1974.

R. Amadio and Y. Régis-gianas, Certifying and Reasoning on Cost Annotations of Functional Programs, Lecture Notes in Computer Science, vol.7177, pp.72-89, 2011.
DOI : 10.1007/978-3-642-32495-6_5

A. Appel, Compiling with Continuations, 1992.
DOI : 10.1017/CBO9780511609619

D. Aspinall, L. Beringer, M. Hofmann, H. Loidl, and A. Momigliano, A program logic for resources, Theoretical Computer Science, vol.389, issue.3, pp.411-445, 2007.
DOI : 10.1016/j.tcs.2007.09.003
URL : https://doi.org/10.1016/j.tcs.2007.09.003

D. Aspinall, M. Hofmann, and M. Kone?ný, A type system with usage aspects, Journal of Functional Programming, vol.7, issue.02, pp.141-178, 2008.
DOI : 10.1016/0304-3975(93)90110-F

R. Atkey, Amortised resource analysis with separation logic, Logical Methods in Computer Science, vol.7, issue.2, p.17, 2011.
DOI : 10.1007/978-3-642-11957-6_6

N. Ayache and R. Amadio, Certifying and Reasoning on Cost Annotations in C Programs, Lecture Notes in Computer Science, vol.7437, pp.32-46
DOI : 10.1007/978-3-642-32469-7_3
URL : https://hal.archives-ouvertes.fr/hal-00702665

H. Baker, List processing in real time on a serial computer, Communications of the ACM, vol.21, issue.4, pp.280-294, 1978.
DOI : 10.1145/359460.359470

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development ? Coq'Art: The Calculus of Inductive Constructions, Theoretical Computer Science. An EATCS Series, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

G. Blelloch and J. Greiner, Parallelism in sequential functional languages, Proceedings of the seventh international conference on Functional programming languages and computer architecture , FPCA '95, pp.226-237, 1995.
DOI : 10.1145/224164.224210
URL : http://www-2.cs.cmu.edu/%7Eguyb/papers/BG95.pdf

Q. Carbonneaux, J. Hoffmann, T. Ramananandro, and Z. Shao, End-to-end verification of stack-space bounds for C programs, Programming Language Design and Implementation (PLDI), pp.270-281, 2014.

A. Charguéraud, Characteristic formulae for mechanized program verification, 2010.

A. Charguéraud, Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation, Lecture Notes in Computer Science, vol.9236, pp.137-153, 2013.
DOI : 10.1007/978-3-319-22102-1_9

A. Charguéraud and F. Pottier, Online accompanying material, 2017.

A. Chlipala, The Bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier, International Conference on Functional Programming (ICFP), pp.391-402, 2013.

A. Chlipala, G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky, Effective interactive proofs for higherorder imperative programs, International Conference on Functional Programming (ICFP), pp.79-90, 2009.
DOI : 10.1145/1596550.1596565

M. Clochard, J. Filliâtre, and A. Paskevich, How to Avoid Proving the Absence of Integer Overflows, Verified Software: Theories, Tools and Experiments, pp.94-109, 2015.
DOI : 10.1007/978-3-319-08867-9_1
URL : https://hal.archives-ouvertes.fr/hal-01162661

S. Conchon and J. Filliâtre, A persistent union-find data structure, Proceedings of the 2007 workshop on Workshop on ML , ML '07, pp.37-46, 2007.
DOI : 10.1145/1292535.1292541
URL : http://www.lri.fr/~filliatr/ftp/publis/puf-wml07.ps

T. Cormen, C. Leiserson, R. Rivest, C. Stein, and S. Weirich, Introduction to Algorithms Resource bound certification, Principles of Programming Languages (POPL), pp.184-198, 2000.

N. Danielsson, Lightweight semiformal time complexity analysis for purely functional data structures, In: Principles of Programming Languages, 2008.
DOI : 10.1145/1328897.1328457

N. Danner, J. Paykin, and J. Royer, A static cost analysis for a higher-order language, Proceedings of the 7th workshop on Programming languages meets program verification, PLPV '13, pp.25-34, 2013.
DOI : 10.1145/2428116.2428123
URL : http://cis.upenn.edu/~jpaykin/papers/danner_PLPV_2013.pdf

V. Dornic, P. Jouvelot, and D. Gifford, Polymorphic time systems for estimating program complexity, ACM Letters on Programming Languages and Systems, vol.1, issue.1, pp.33-45, 1992.
DOI : 10.1145/130616.130620
URL : http://tesla.lcs.mit.edu/publications/Papers/loplas.ps

Z. Galil and G. Italiano, Data structures and algorithms for disjoint set union problems, ACM Computing Surveys, vol.23, issue.3, pp.319-344, 1991.
DOI : 10.1145/116873.116878

B. Galler and M. Fischer, An improved equivalence algorithm, Communications of the ACM, vol.7, issue.5, pp.301-303, 1964.
DOI : 10.1145/364099.364331

A. Guéneau, M. Myreen, R. Kumar, and M. Norrish, Verified Characteristic Formulae for CakeML, European Symposium on Programming, pp.584-610, 2017.
DOI : 10.1145/2429069.2429121

G. Harfst and E. Reingold, A potential-based amortized analysis of the union-find data structure, ACM SIGACT News, vol.31, issue.3, pp.86-95, 2000.
DOI : 10.1145/356458.356463

J. Hoffmann and M. Hofmann, Amortized Resource Analysis with Polynomial Potential, European Symposium on Programming, pp.287-306, 2010.
DOI : 10.1007/978-3-642-11957-6_16

J. Hoffmann, K. Aehlig, and M. Hofmann, Multivariate amortized resource analysis, ACM Transactions on Programming Languages and Systems, vol.3414, issue.3, pp.1-1462, 2012.
DOI : 10.1145/1925844.1926427
URL : http://www.tcs.ifi.lmu.de/%7Ehoffmann/papers/aa_popl11.pdf

J. Hoffmann, M. Marmar, and Z. Shao, Quantitative Reasoning for Proving Lock-Freedom, 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, pp.124-133, 2013.
DOI : 10.1109/LICS.2013.18
URL : http://flint.cs.yale.edu/flint/publications/lockfree-tr.pdf

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

M. Hofmann, A type system for bounded space and functional in-place update, Nordic Journal of Computing, vol.7, issue.4, pp.258-289, 2000.

M. Hofmann and S. Jost, Static prediction of heap space usage for first-order functional programs, Principles of Programming Languages (POPL), pp.185-197, 2003.

J. Hopcroft and J. Ullman, Set Merging Algorithms, SIAM Journal on Computing, vol.2, issue.4, pp.294-303, 1973.
DOI : 10.1137/0202024

R. Howell, On asymptotic notation with multiple variables. Tech. Rep. 2007-4, Kansas State Univer- sity Howell RR (2012) Algorithms: A top-down approach. Draft Hutton G (1999) A tutorial on the universality and expressiveness of fold, Journal of Functional Programming, vol.9, issue.4, pp.355-372, 2008.

R. Jung, D. Swasey, F. Sieczkowski, K. Svendsen, A. Turon et al., Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning, Principles of Programming Languages (POPL), pp.637-650, 2015.

R. Jung, R. Krebbers, L. Birkedal, and D. Dreyer, Higher-order ghost state, International Conference on Functional Programming (ICFP), pp.256-269, 2016.
DOI : 10.1145/3022670.2951943

H. Kaplan, N. Shafrir, and R. Tarjan, Union-find with deletions, Symposium on Discrete Algorithms (SODA), pp.19-28, 2002.

D. Kozen, R. Krebbers, R. Jung, A. Bizjak, J. Jourdan et al., The design and analysis of algorithms. Texts and Monographs in Computer Science The essence of higher-order concurrent separation logic, European Symposium on Programming (ESOP), pp.696-723, 1992.

N. Krishnaswami, Verifying higher-order imperative programs with higher-order separation logic) A separation logic framework for Imperative HOL. Archive of Formal Proofs Le Métayer D (1988) ACE: an automatic complexity evaluator, ACM Transactions on Programming Languages and Systems, vol.10, issue.2, pp.248-266, 2012.

K. Leino and M. Moskal, VACID-0: Verification of ample correctness of invariants of data-structures, p.209, 2010.

K. Mackenzie and N. Wolverson, Camelot and Grail: resource-aware functional programming for the JVM, In: Trends in Functional Programming (TFP), vol.4, pp.29-46, 2003.

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.
DOI : 10.1145/3093333.3009874

J. Mccarthy, B. Fetscher, M. New, D. Feltey, and R. Findler, A Coq Library for Internal Verification of Running-Times, Functional and Logic Programming, pp.144-162, 2016.
DOI : 10.1007/978-3-642-02444-3_16

P. Müller, M. Schwerhoff, and A. Summers, Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution, Computer Aided Verification (CAV), pp.405-425, 2016.
DOI : 10.1007/978-3-642-36946-9_14

A. Nanevski, A. Ahmed, G. Morrisett, and L. Birkedal, Abstract Predicates and Mutable ADTs in Hoare Type Theory, European Symposium on Programming (ESOP), pp.189-204, 2007.
DOI : 10.1007/978-3-540-71316-6_14

A. Nanevski, G. Morrisett, and L. Birkedal, Hoare type theory, polymorphism and separation, Journal of Functional Programming, vol.18, pp.5-6865, 2008.

A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal, Ynot: dependent types for imperative programs, International Conference on Functional Programming (ICFP), pp.229-240, 2008.

T. Nipkow, Amortized Complexity Verified, Interactive Theorem Proving (ITP) Lecture Notes in Computer Science, vol.9236, pp.310-324, 2015.
DOI : 10.1007/978-3-319-22102-1_21

C. Okasaki, M. Patwary, J. Blair, and F. Manne, Purely Functional Data Structures Experiments on union-find algorithms for the disjoint-set data structure, International Symposium on Experimental Algorithms (SEA), pp.411-423, 1999.

A. Pilkiewicz and F. Pottier, The essence of monotonic state, Proceedings of the 7th ACM SIGPLAN workshop on Types in language design and implementation, TLDI '11, 2011.
DOI : 10.1145/1929553.1929565
URL : https://hal.archives-ouvertes.fr/hal-01081193

B. Reistad and D. Gifford, Static dependent costs for estimating execution time, ACM Symposium on Lisp and Functional Programming (LFP), pp.65-78, 1994.
DOI : 10.1145/182409.182439
URL : http://www.cise.ufl.edu/~juin/researchPapers/Reistad94.pdf

J. Reynolds, Separation logic: a logic for shared mutable data structures, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp.55-74, 2002.
DOI : 10.1109/LICS.2002.1029817

D. Sands, J. Gustavsson, and A. Moran, Lambda Calculi and Linear Speedups, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones Lecture Notes in Computer Science, vol.2566, pp.60-84, 2002.
DOI : 10.1007/3-540-36377-7_4
URL : http://w2.cadence.com/company/cadence_labs/jorgeng_EC_2002_Lambda.pdf

R. Seidel and M. Sharir, Top-Down Analysis of Path Compression, SIAM Journal on Computing, vol.34, issue.3, pp.515-525, 2005.
DOI : 10.1137/S0097539703439088

R. Tarjan, Efficiency of a Good But Not Linear Set Union Algorithm, Journal of the ACM, vol.22, issue.2, pp.215-225, 1975.
DOI : 10.1145/321879.321884

R. Tarjan, Amortized Computational Complexity, SIAM Journal on Algebraic Discrete Methods, vol.6, issue.2, pp.306-318, 1985.
DOI : 10.1137/0606031

R. Tarjan, Worst-case Analysis of Set Union Algorithms, Journal of the ACM, vol.31, issue.2, pp.245-281, 1999.
DOI : 10.1145/62.2160
URL : http://www.csd.uwo.ca/~eschost/Teaching/07-08/CS445a/p245-tarjan.pdf