M. Korp and A. Middeldorp, Match-bounds revisited Information and Computation, pp.1259-1283

G. Moser and A. Schnabl, The derivational complexity induced by the dependency pair method, Logical Methods in Computer Science, vol.7, issue.3131, pp.1-38, 2011.

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL ? A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science, pp.10-1007, 2002.

L. Noschinski, F. Emmes, and J. Giesl, Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs, Journal of Automated Reasoning, vol.19, issue.2, pp.27-56
DOI : 10.1007/s10817-013-9277-6

C. Sternagel and R. Thiemann, Certified subterm criterion and certified usable rules, Proc. 21st International Conference on Rewriting Techniques and Applications of Leibniz International Proceedings in Informatics, pp.325-340, 2010.

C. Sternagel and R. Thiemann, Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs, Proc. Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications, pp.441-455
DOI : 10.1007/978-3-319-08918-8_30

R. Thiemann and C. Sternagel, Certification of Termination Proofs Using CeTA, Proc. 22nd International Conference on Theorem Proving in Higher Order Logics, pp.452-468978, 1007.
DOI : 10.1007/978-3-540-25979-4_6

H. Zankl and M. Korp, Modular complexity analysis via relative complexity, Proc. 21st International Conference on Rewriting Techniques and Applications of Leibniz International Proceedings in Informatics, pp.385-400, 2010.

H. Zankl and M. Korp, Modular Complexity Analysis for Term Rewriting, Logical Methods in Computer Science, vol.10, issue.1, pp.1-34
DOI : 10.2168/LMCS-10(1:19)2014