{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:48:52Z","timestamp":1767926932419,"version":"3.49.0"},"reference-count":94,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T00:00:00Z","timestamp":1309478400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2011,8]]},"abstract":"<jats:p>Termination is an important property of programs, and is notably required for programs formulated in proof assistants. It is a very active subject of research in the Turing-complete formalism of term rewriting. Over the years, many methods and tools have been developed to address the problem of deciding termination for specific problems (since it is undecidable in general). Ensuring the reliability of those tools is therefore an important issue.<\/jats:p><jats:p>In this paper we present a library formalising important results of the theory of well-founded (rewrite) relations in the proof assistant Coq. We also present its application to the automated verification of termination certificates, as produced by termination tools.<\/jats:p><jats:p>The sources are freely available at<jats:uri xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:type=\"simple\" xlink:href=\"http:\/\/color.inria.fr\/\">http:\/\/color.inria.fr\/<\/jats:uri>.<\/jats:p>","DOI":"10.1017\/s0960129511000120","type":"journal-article","created":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T14:53:35Z","timestamp":1309532015000},"page":"827-859","source":"Crossref","is-referenced-by-count":33,"title":["CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates"],"prefix":"10.1017","volume":"21","author":[{"given":"FR\u00c9D\u00c9RIC","family":"BLANQUI","sequence":"first","affiliation":[]},{"given":"ADAM","family":"KOPROWSKI","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2011,7,1]]},"reference":[{"key":"S0960129511000120_ref94","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/FI-1995-24124","article-title":"Termination of Term Rewriting by Semantic Labelling.","volume":"24","author":"Zantema","year":"1995","journal-title":"Fundamenta Informaticae"},{"key":"S0960129511000120_ref91","unstructured":"Waldmann J. (2008) Report on the Termination Competition. Proceedings of WST'09. (Available at http:\/\/www.imn.htwk-leipzig.de\/~waldmann\/talk\/09\/wst\/paper.pdf.)"},{"key":"S0960129511000120_ref90","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_31"},{"key":"S0960129511000120_ref89","volume-title":"Term Rewriting Systems","year":"2003"},{"key":"S0960129511000120_ref87","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15205-4_40"},{"key":"S0960129511000120_ref85","unstructured":"Sternagel C. , Thiemann R. , Winkler S. and Zankl H. (2010) CeTA."},{"key":"S0960129511000120_ref83","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70590-1_23"},{"key":"S0960129511000120_ref81","doi-asserted-by":"publisher","DOI":"10.1145\/1291220.1291156"},{"key":"S0960129511000120_ref80","doi-asserted-by":"publisher","DOI":"10.1145\/1614431.1614433"},{"key":"S0960129511000120_ref79","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74621-8_18"},{"key":"S0960129511000120_ref78","first-page":"292","volume-title":"Proceedings of the 24th Annual ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages \u2013 POPL'97","author":"Sa\u00efbi","year":"1997"},{"key":"S0960129511000120_ref77","volume-title":"Haskell 98 Language and Libraries, The revised report","author":"Peyton-Jones","year":"2003"},{"key":"S0960129511000120_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74621-8_10"},{"key":"S0960129511000120_ref58","first-page":"263","volume-title":"Computational problems in abstract algebra","author":"Knuth","year":"1970"},{"key":"S0960129511000120_ref60","unstructured":"Koprowski A. (2008) Termination of rewriting and its certification, Ph.D. thesis, Technische Universiteit Eindhoven, The Netherlands."},{"key":"S0960129511000120_ref82","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"S0960129511000120_ref88","doi-asserted-by":"crossref","unstructured":"Strub P.-Y. (2010b) Coq modulo theories. (Available at http:\/\/pierre-yves.strub.nu\/research\/coqmt\/.)","DOI":"10.1007\/978-3-642-15205-4_40"},{"key":"S0960129511000120_ref36","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1067620188"},{"key":"S0960129511000120_ref32","first-page":"377","volume-title":"Logic for Programming and Automated Reasoning: Proceedings of LPAR'00","author":"Delahaye","year":"2000"},{"key":"S0960129511000120_ref63","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77566-9_28"},{"key":"S0960129511000120_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90026-3"},{"key":"S0960129511000120_ref29","first-page":"50","volume-title":"Proceedings of COLOG'88","author":"Coquand","year":"1988"},{"key":"S0960129511000120_ref9","unstructured":"Blanqui F. (2006) Higher-order dependency pairs. Proceedings of WST'06."},{"key":"S0960129511000120_ref75","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75285"},{"key":"S0960129511000120_ref52","unstructured":"Hinderer S. (2004) Certification des preuves de terminaison par interpr\u00e9tations polynomiales, M.Phil. thesis, Universit\u00e9 Henri Poincar\u00e9, Nancy, France."},{"key":"S0960129511000120_ref51","unstructured":"Harper R. , MacQueen D. and Milner R. (1986) Standard ML. Technical report ECS-LFCS-86-2. University of Edinburgh, U.K."},{"key":"S0960129511000120_ref56","unstructured":"Hur C.-K. (2009) Heq: A Coq library for Heterogeneous Equality."},{"key":"S0960129511000120_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-09680-3_24"},{"key":"S0960129511000120_ref93","unstructured":"Werner B. (1994) Une Th\u00e9orie des Constructions Inductives, Ph.D. thesis, Universit\u00e9 Paris VII."},{"key":"S0960129511000120_ref55","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_32"},{"key":"S0960129511000120_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/1160074.1159825"},{"key":"S0960129511000120_ref45","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9057-7"},{"key":"S0960129511000120_ref68","unstructured":"Leroy X. , Doligez D. , Frisch A. , Garrigue J. , R\u00e9my D. and Vouillon J. (2010) The Objective Caml system release 3.12, Documentation and user's manual. INRIA, France."},{"key":"S0960129511000120_ref71","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00011-7"},{"key":"S0960129511000120_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/s00200-006-0020-y"},{"key":"S0960129511000120_ref18","first-page":"163","volume-title":"Proceedings Interactive Theorem Proving, ITP 2010","author":"Braibant","year":"2010"},{"key":"S0960129511000120_ref3","first-page":"146","volume-title":"Proceedings 13th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2000)","author":"Balaa","year":"2000"},{"key":"S0960129511000120_ref66","doi-asserted-by":"publisher","DOI":"10.1007\/10704567_3"},{"key":"S0960129511000120_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9087-9"},{"key":"S0960129511000120_ref13","unstructured":"Blanqui F. , Coupet-Grimal S. , Delobel W. , Hinderer S. and Koprowski A. (2006) CoLoR: a Coq Library on Rewriting and termination. Proceedings of WST'06."},{"key":"S0960129511000120_ref61","doi-asserted-by":"publisher","DOI":"10.1007\/s00200-009-0105-5"},{"key":"S0960129511000120_ref73","first-page":"8","volume-title":"Logic-Based Program Synthesis and Transformation: Proceedings of LOPSTR'07","author":"Nguyen","year":"2007"},{"key":"S0960129511000120_ref92","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(3:8)2008"},{"key":"S0960129511000120_ref19","unstructured":"Briais S. (2008) Theory and Tool Support for the Formal Verification of Cryptographic Protocols, Ph.D. thesis, \u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne, Switzerland."},{"key":"S0960129511000120_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_23"},{"key":"S0960129511000120_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00207-8"},{"key":"S0960129511000120_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/S095679689700289X"},{"key":"S0960129511000120_ref6","first-page":"114","volume-title":"Proceedings of FLOPS'06","volume":"3945","author":"Barthe","year":"2006"},{"key":"S0960129511000120_ref5","volume-title":"Handbook of logic in computer science","author":"Barendregt","year":"1992"},{"key":"S0960129511000120_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_33"},{"key":"S0960129511000120_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45842-5_2"},{"key":"S0960129511000120_ref10","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004426"},{"key":"S0960129511000120_ref65","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_34"},{"key":"S0960129511000120_ref86","unstructured":"Streicher T. (1993) Investigations into Intensional Type Theory, Habilitation Thesis, Technical report, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, Germany."},{"key":"S0960129511000120_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_18"},{"key":"S0960129511000120_ref11","volume-title":"Rewriting, Computation and Proof \u2013 Essays Dedicated to J.-P. Jouannaud on the Occasion of His 60th Birthday","author":"Blanqui","year":"2007"},{"key":"S0960129511000120_ref12","unstructured":"Blanqui F. and Koprowski A. (2009) Automated verification of termination certificates. Technical report 6949, INRIA Rocquencourt, France."},{"key":"S0960129511000120_ref1","unstructured":"Altenkirch T. (1993) Constructions, Inductive Types and Strong Normalization, Ph.D. thesis, University of Edinburgh."},{"key":"S0960129511000120_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74915-8_26"},{"key":"S0960129511000120_ref16","unstructured":"Boespflug M. (2010) Dedukti version 1.1.3. (Available at http:\/\/www.lix.polytechnique.fr\/dedukti\/.)"},{"key":"S0960129511000120_ref17","unstructured":"Borovansk\u00fd P. , Cirstea H. , Dubois H. , Kirchner C. , Kirchner H. , Moreau P.-E. , Ringeissen C. and Vittek M. (2000) ELAN User Manual. INRIA Nancy, France."},{"key":"S0960129511000120_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_5"},{"key":"S0960129511000120_ref54","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.08.010"},{"key":"S0960129511000120_ref23","unstructured":"Clavel M. , Dur\u00e1n F. , Eker S. , Lincoln P. , Mart\u00ed-Oliet N. , Meseguer J. and Talcott C. (2005) Maude Manual (Version 2.2). Computer Science Laboratory, SRI International and Department of Computer Science, University of Illinois at Urbana-Champaign, U.S.A."},{"key":"S0960129511000120_ref24","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1007\/978-3-540-73147-4_13","volume-title":"Rewriting, Computation and Proof \u2013 Essays Dedicated to J.-P. Jouannaud for his 60th Birthday","author":"Contejean","year":"2007"},{"key":"S0960129511000120_ref76","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037116"},{"key":"S0960129511000120_ref74","unstructured":"Nipkow T. , Paulson L. and Wenzel M. (2002) Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag Lecture Notes in Computer Science 2283."},{"key":"S0960129511000120_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-9022-x"},{"key":"S0960129511000120_ref8","volume-title":"Coq'Art: The Calculus of Inductive Constructions","author":"Bertot","year":"2004"},{"key":"S0960129511000120_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_17"},{"key":"S0960129511000120_ref59","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_17"},{"key":"S0960129511000120_ref27","unstructured":"Coq Development Team (2009) The Coq Reference Manual, Version 8.2. INRIA, France."},{"key":"S0960129511000120_ref35","volume-title":"Handbook of Theoretical Computer Science","author":"Dershowitz","year":"1990"},{"key":"S0960129511000120_ref37","doi-asserted-by":"publisher","DOI":"10.1023\/A:1027357912519"},{"key":"S0960129511000120_ref38","unstructured":"Contejean E. , March\u00e9 C. and Urbain X. (2009) CiME version 3."},{"key":"S0960129511000120_ref41","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2002.0541"},{"key":"S0960129511000120_ref28","unstructured":"Coquand T. (1992) Pattern Matching with Dependent Types. In: Nordstr\u00f6m B. , Petersson K. and Plotkin G. (eds.) Proceedings of the 1992 Workshop on Types for Proofs and Programs."},{"key":"S0960129511000120_ref69","first-page":"200","volume-title":"Types for Proofs and Programs: Proceedings of TYPES'02","author":"Letouzey","year":"2002"},{"key":"S0960129511000120_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_24"},{"key":"S0960129511000120_ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39813-4_11"},{"key":"S0960129511000120_ref46","first-page":"39","volume-title":"Types for Proofs and Programs: International Workshop TYPES '94","author":"Gim\u00e9nez","year":"1994"},{"key":"S0960129511000120_ref47","volume-title":"Proofs and Types","author":"Girard","year":"1988"},{"key":"S0960129511000120_ref84","first-page":"325","article-title":"Certified Subterm Criterion and Certified Usable Rules","volume":"6","author":"Sternagel","year":"2010","journal-title":"Leibniz International Proceedings in Informatics"},{"key":"S0960129511000120_ref48","unstructured":"Gonthier G. and Mahboubi A. (2009) A Small Scale Reflection extension for the Coq system. Technical report 6455. INRIA and Microsoft Research. Version 4."},{"key":"S0960129511000120_ref33","first-page":"67","volume-title":"Logic Programming: Proceedings of ICLP'04","author":"Dershowitz","year":"2004"},{"key":"S0960129511000120_ref49","doi-asserted-by":"publisher","DOI":"10.1145\/583852.581501"},{"key":"S0960129511000120_ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_9"},{"key":"S0960129511000120_ref53","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2004.10.004"},{"key":"S0960129511000120_ref70","unstructured":"Manna Z. and Ness S. (1970) On the termination of Markov algorithms. In: Proceedings 3rd Hawaii International Conference on System Science 789\u2013792."},{"key":"S0960129511000120_ref57","first-page":"402","volume-title":"LICS '99 Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science","author":"Jouannaud","year":"1999"},{"key":"S0960129511000120_ref62","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70590-1_14"},{"key":"S0960129511000120_ref64","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02348-4_21"},{"key":"S0960129511000120_ref67","unstructured":"Lankford D. (1979) On Proving term rewriting systems are Noetherian. Technical report Lousiana Technical University, USA."},{"key":"S0960129511000120_ref72","unstructured":"McBride C. (1999) Dependently typed functional programs and their proofs, Ph.D. thesis, University of Edinburgh."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129511000120","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,21]],"date-time":"2020-06-21T01:50:25Z","timestamp":1592704225000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129511000120\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7,1]]},"references-count":94,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011,8]]}},"alternative-id":["S0960129511000120"],"URL":"https:\/\/doi.org\/10.1017\/s0960129511000120","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,7,1]]}}}