Hostname: page-component-745bb68f8f-hvd4g Total loading time: 0 Render date: 2025-02-03T11:22:58.999Z Has data issue: false hasContentIssue false
  • English
  • Français

CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates

Published online by Cambridge University Press:  01 July 2011

FRÉDÉRIC BLANQUI  and
ADAM KOPROWSKI
FRÉDÉRIC BLANQUI
Affiliation:
INRIA, FIT 3-604, Tsinghua University, Haidian District, Beijing 100084, China Email: [email protected]
ADAM KOPROWSKI
Affiliation:
MLstate, 15 Rue Berlier, 75013 Paris, France Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

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.

The sources are freely available at http://color.inria.fr/.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 21 , Special Issue 4: Interactive Theorem Proving and the Formalisation of Mathematics , August 2011 , pp. 827 - 859
Copyright
Copyright © Cambridge University Press 2011

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Altenkirch, T. (1993) Constructions, Inductive Types and Strong Normalization, Ph.D. thesis, University of Edinburgh.Google Scholar
Arts, T. and Giesl, J. (2000) Termination of Term Rewriting Using Dependency Pairs. Theoretical Computer Science 236 133–178.CrossRefGoogle Scholar
Balaa, A. and Bertot, Y. (2000) Fix-Point Equations for Well-Founded Recursion in Type Theory. In: Harrison, J. and Aagaard, M. (eds.) Proceedings 13th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2000). Springer-Verlag Lecture Notes in Computer Science 1869146–162.Google Scholar
Barbanera, F., Fernández, M. and Geuvers, H. (1997) Modularity of strong normalization in the algebraic-λ-cube. Journal of Functional Programming 7 (6)613–660.CrossRefGoogle Scholar
Barendregt, H. (1992) Lambda Calculi with types. In: Abramsky, S., Gabbay, D. and Maibaum, T. (eds.) Handbook of logic in computer science 2, Oxford University Press.Google Scholar
Barthe, G., Forest, J., Pichardie, D. and Rusu, V. (2006) Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. In: Hagiya, M. et al. . (eds.) Proceedings of FLOPS'06. Springer-Verlag Lecture Notes in Computer Science 3945 114–129.Google Scholar
Berghofer, S. and Nipkow, T. (2002) Executing Higher Order Logic. In: Geuvers, H. and Wiedijk, F. (eds.) Types for Proofs and Programs: Proceedings of TYPES'02. Springer-Verlag Lecture Notes in Computer Science 264624–40.CrossRefGoogle Scholar
Bertot, Y. and Castéran, P. (2004) Coq'Art: The Calculus of Inductive Constructions, EATCS Texts in Theoretical Computer Science, Springer-Verlag.Google Scholar
Blanqui, F. (2006) Higher-order dependency pairs. Proceedings of WST'06.Google Scholar
Blanqui, F. (2005) Definitions by rewriting in the Calculus of Constructions. Mathematical Structures in Computer Science 15 (1)37–92.CrossRefGoogle Scholar
Blanqui, F. (2007) Computability Closure: Ten Years Later. In: Comon-Lundh, H., Kirchner, C. and Kirchner, H. (eds.) Rewriting, Computation and Proof – Essays Dedicated to J.-P. Jouannaud on the Occasion of His 60th Birthday. Springer-Verlag Lecture Notes in Computer Science 4600.Google Scholar
Blanqui, F. and Koprowski, A. (2009) Automated verification of termination certificates. Technical report 6949, INRIA Rocquencourt, France.Google Scholar
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.Google Scholar
Blanqui, F., Jouannaud, J.-P. and Strub, P.-Y. (2007) Building Decision Procedures in the Calculus of Inductive Constructions. In: Duparc, J. and Henzinger, T. (eds.) Computer Science Logic: Proceedings of CSL'07. Springer-Verlag Lecture Notes in Computer Science 4646328–342.CrossRefGoogle Scholar
Blanqui, F., Jouannaud, J.-P. and Strub, P.-Y. (2008) From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures. In: Ausiello, G., Karhumäki, J., Mauri, G. and Ong, L. (eds.) Fifth IFIP International Conference on Theoretical Computer Science – TCS 2008, IFIP Advances in Information and Communication Technology 273, Springer-Verlag 349–365.CrossRefGoogle Scholar
Boespflug, M. (2010) Dedukti version 1.1.3. (Available at http://www.lix.polytechnique.fr/dedukti/.)Google Scholar
Borovanský, P., Cirstea, H., Dubois, H., Kirchner, C., Kirchner, H., Moreau, P.-E., Ringeissen, C. and Vittek, M. (2000) ELAN User Manual. INRIA Nancy, France.Google Scholar
Braibant, T. and Pous, D. (2010) An efficient Tactic for Deciding Kleene Algebras. In: Kaufmann, M. and Paulson, L. (eds.) Proceedings Interactive Theorem Proving, ITP 2010. Springer-Verlag Lecture Notes in Computer Science 6172163–178.Google Scholar
Briais, S. (2008) Theory and Tool Support for the Formal Verification of Cryptographic Protocols, Ph.D. thesis, École Polytechnique Fédérale de Lausanne, Switzerland.Google Scholar
Bulwahn, L., Krauss, A. and Nipkow, T. (2007) Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL. In: Schneider, K. and Brandt, J. (eds.) Proceedings 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007). Springer-Verlag Lecture Notes in Computer Science 473238–53.Google Scholar
Chlipala, A. (2006) Modular Development of Certified Program Verifiers with a Proof Assistant. Proceedings of ICFP'06. SIGPLAN Notices 41 (9).CrossRefGoogle Scholar
Chrząszcz, J. (2003) Implementation of Modules in the Coq System. In: Basin, D. and Wolff, B. (eds.) Proceedings 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003). Springer-Verlag Lecture Notes in Computer Science 2758270–286.CrossRefGoogle Scholar
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-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.Google Scholar
Contejean, E. (2007) Modelling permutations in Coq for Coccinelle. In: Comon-Lundh, H., Kirchner, C. and Kirchner, H. (eds.) Rewriting, Computation and Proof – Essays Dedicated to J.-P. Jouannaud for his 60th Birthday. Springer-Verlag Lecture Notes in Computer Science 4600259–269.CrossRefGoogle Scholar
Contejean, E., Courtieu, P., Forest, J., Pons, O. and Urbain, X. (2007) Certification of automated termination proofs. In: Konev, B. and Wolter, F. (eds.) Frontiers of Combining Systems: Proceedings of FROCOS'07. Springer-Verlag Lecture Notes in Computer Science 4720148–162.CrossRefGoogle Scholar
Contejean, E., Marché, C., Tomás, A. P. and Urbain, X. (2005) Mechanically proving termination using polynomial interpretations. Journal of Automated Reasoning 34 (4)325–363.CrossRefGoogle Scholar
Coq Development Team (2009) The Coq Reference Manual, Version 8.2. INRIA, France.Google Scholar
Coquand, T. (1992) Pattern Matching with Dependent Types. In: Nordström, B., Petersson, K. and Plotkin, G. (eds.) Proceedings of the 1992 Workshop on Types for Proofs and Programs.Google Scholar
Coquand, T. and Paulin, C. (1988) Inductively defined types. In: Martin-Löf, P. and Mints, G. (eds.) Proceedings of COLOG'88. Springer-Verlag Lecture Notes in Computer Science 41750–66.Google Scholar
Coupet-Grimal, S. and Delobel, W. (2006) An Effective Proof of the Well-Foundedness of the Multiset Path Ordering. AAECC 17 (6)453–469.CrossRefGoogle Scholar
Courtieu, P., Forest, J. and Urbain, X. (2008) Certifying a Termination Criterion Based on Graphs, without Graphs. In: Mohamed, O. A., Muñoz, C. and Tahar, S. (eds.) Proceedings 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008). Springer-Verlag Lecture Notes in Computer Science 5170183–198.CrossRefGoogle Scholar
Delahaye, D. (2000) A Tactic Language for the System Coq. In: Parigot, M. and Voronkov, A. (eds.) Logic for Programming and Automated Reasoning: Proceedings of LPAR'00. Springer-Verlag Lecture Notes in Computer Science 1955377–440.Google Scholar
Dershowitz, N. (2004) Termination by abstraction. In: Demoen, B. and Lifschitz, V. (eds.) Logic Programming: Proceedings of ICLP'04. Springer-Verlag Lecture Notes in Computer Science 313267–93.Google Scholar
Dershowitz, N. (1982) Orderings for term rewriting systems. Theoretical Computer Science 17 279–301.CrossRefGoogle Scholar
Dershowitz, N. and Jouannaud, J.-P. (1990) Rewrite Systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, volume B, Chapter 6, North-Holland.Google Scholar
Dowek, G. and Werner, B. (2003) Proof normalization modulo. Journal of Symbolic Logic 68 (4)1289–1316.CrossRefGoogle Scholar
Dowek, G., Hardin, T. and Kirchner, C. (2003) Theorem proving modulo. Journal of Automated Reasoning 31 33–72.CrossRefGoogle Scholar
Contejean, E., Marché, C. and Urbain, X. (2009) CiME version 3.Google Scholar
Endrullis, J., Waldmann, J. and Zantema, H. (2008) Matrix Interpretations for Proving Termination of Term Rewriting. Journal of Automated Reasoning 40 (2–3)195–220.CrossRefGoogle Scholar
Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R. and Zankl, H. (2007) SAT Solving for Termination Analysis with Polynomial Interpretations. In: Marques-Silva, J. and Sakallah, K. (eds.) Theory and Applications of Satisfiability Testing – Proceedings of SAT 2007. Springer-Verlag Lecture Notes in Computer Science 4501340–354.CrossRefGoogle Scholar
Giesl, J., Arts, T. and Ohlebusch, E. (2002) Modular termination proofs for rewriting using dependency pairs. Journal of Symbolic Computation 34 (1)21–58.CrossRefGoogle Scholar
Giesl, J., Schneider-Kamp, P. and Thiemann, R. (2006) AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework. In: Furbach, U. and Shankar, N. (eds.) Automated Reasoning: Proceedings of IJCAR'06. Springer-Verlag Lecture Notes in Computer Science 4130281–286.CrossRefGoogle Scholar
Giesl, J., Swiderski, S., Schneider-Kamp, P. and Thiemann, R. (2006) Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages. In: Pfenning, F. (ed.) Term Rewriting and Applications: Proceedings of RTA'06. Springer-Verlag Lecture Notes in Computer Science 4098297–312.CrossRefGoogle Scholar
Giesl, J., Thiemann, R., Schneider-Kamp, P. and Falke, S. (2003) Improving dependency pairs. In: Vardi, M. Y. and Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence and Reasoning: Proceedings of LPAR'03. Springer-Verlag Lecture Notes in Computer Science 2850167–182.CrossRefGoogle Scholar
Giesl, J., Thiemann, R., Schneider-Kamp, P. and Falke, S. (2006) Mechanizing and Improving Dependency Pairs. Journal of Automated Reasoning 37 (3)155–203.CrossRefGoogle Scholar
Giménez, E. (1994) Codifying Guarded Definitions with Recursion Schemes. In: Dybjer, P., Nordström, B. and Smith, J. (eds.) Types for Proofs and Programs: International Workshop TYPES '94. Springer-Verlag Lecture Notes in Computer Science 99639–59.Google Scholar
Girard, J.-Y., Lafont, Y. and Taylor, P. (1988) Proofs and Types, Cambridge University Press.Google Scholar
Gonthier, G. and Mahboubi, A. (2009) A Small Scale Reflection extension for the Coq system. Technical report 6455. INRIA and Microsoft Research. Version 4.Google Scholar
Grégoire, B. and Leroy, X. (2002) A compiled implementation of strong reduction. Proceedings of ICFP'02. SIGPLAN Notices 37 (9).CrossRefGoogle Scholar
Haftmann, F. and Nipkow, T. (2010) Code Generation via Higher-Order Rewrite Systems. In: Blume, M., Kobayashi, N. and Vidal, G. (eds.) Functional and Logic Programming: Proceedings of FLOPS'10. Springer-Verlag Lecture Notes in Computer Science 6009103–117.CrossRefGoogle Scholar
Harper, R., MacQueen, D. and Milner, R. (1986) Standard ML. Technical report ECS-LFCS-86-2. University of Edinburgh, U.K.Google Scholar
Hinderer, S. (2004) Certification des preuves de terminaison par interprétations polynomiales, M.Phil. thesis, Université Henri Poincaré, Nancy, France.Google Scholar
Hirokawa, N. and Middeldorp, A. (2005) Automating the Dependency Pair Method. Information and Computation 199 (1–2)172–199.CrossRefGoogle Scholar
Hirokawa, N. and Middeldorp, A. (2007) Tyrolean Termination Tool: Techniques and Features. Information and Computation 205 (4)474–511.CrossRefGoogle Scholar
Hirokawa, N. and Moser, G. (2008) Automated complexity analysis based on the dependency pair method. In: Armando, A., Baumgartner, P. and Dowek, G. (eds.) Automated Reasoning: Proceedings of IJCAR'08. Springer-Verlag Lecture Notes in Computer Science 5195364–379.CrossRefGoogle Scholar
Hur, C.-K. (2009) Heq: A Coq library for Heterogeneous Equality.Google Scholar
Jouannaud, J.-P. and Rubio, A. (1999) The Higher-Order Recursive Path Ordering. LICS '99 Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science IEEE Computer Society 402–411.Google Scholar
Knuth, D. and Bendix, P. (1970) Simple word problems in universal algebra. In: Leech, J. (ed.) Computational problems in abstract algebra, Pergamon Press 263–297.Google Scholar
Koprowski, A. (2006) Certified Higher-Order Recursive Path Ordering. In: Pfenning, F. (ed.) Term Rewriting and Applications: Proceedings of RTA'06. Springer-Verlag Lecture Notes in Computer Science 4098227–241.CrossRefGoogle Scholar
Koprowski, A. (2008) Termination of rewriting and its certification, Ph.D. thesis, Technische Universiteit Eindhoven, The Netherlands.Google Scholar
Koprowski, A. (2009) Coq formalization of the higher-order recursive path ordering. Applicable Algebra in Engineering, Communication and Computing 20 (5–6)379–425.CrossRefGoogle Scholar
Koprowski, A. and Waldmann, J. (2008) Arctic Termination. . . Below Zero. In: Voronkov, A. (ed.) Rewriting Techniques and Applications: Proceedings of RTA'08. Springer-Verlag Lecture Notes in Computer Science 5117202–216.CrossRefGoogle Scholar
Koprowski, A. and Zantema, H. (2008) Certification of Proving Termination of Term Rewriting by Matrix Interpretations. In: Geffert, V. et al. (eds.) SOFSEM 2008: Theory and Practice of Computer Science. Springer-Verlag Lecture Notes in Computer Science 4910328–339.CrossRefGoogle Scholar
Korp, M., Sternagel, C., Zankl, H. and Middeldorp, A. (2009) Tyrolean Termination Tool 2. In: Treinen, R. (ed.) Rewriting Techniques and Applications: Proceedings of RTA'09. Springer-Verlag Lecture Notes in Computer Science 5595295–304.CrossRefGoogle Scholar
Krauss, A. (2007) Certified Size-Change Termination. In: Pfenning, F. (ed.) Automated Deduction – CADE-21. Springer-Verlag Lecture Notes in Computer Science 4603460–475.CrossRefGoogle Scholar
Kusakari, K., Nakamura, M. and Toyama, Y. (1999) Argument Filtering Transformation. In: Nadathur, G. (ed.) Principles and Practice of Declarative Programming: Proceedings of PPDP'99. Springer-Verlag Lecture Notes in Computer Science 170247–61.CrossRefGoogle Scholar
Lankford, D. (1979) On Proving term rewriting systems are Noetherian. Technical report Lousiana Technical University, USA.Google Scholar
Leroy, X., Doligez, D., Frisch, A., Garrigue, J., Rémy, D. and Vouillon, J. (2010) The Objective Caml system release 3.12, Documentation and user's manual. INRIA, France.Google Scholar
Letouzey, P. (2002) A New Extraction for Coq. In: Geuvers, H. and Wiedijk, F. (eds.) Types for Proofs and Programs: Proceedings of TYPES'02. Springer-Verlag Lecture Notes in Computer Science 2646200–219.Google Scholar
Manna, Z. and Ness, S. (1970) On the termination of Markov algorithms. In: Proceedings 3rd Hawaii International Conference on System Science 789–792.Google Scholar
Marion, J.-Y. (2003) Analysing the implicit complexity of programs. Information and Computation 183 (1)2–18.CrossRefGoogle Scholar
McBride, C. (1999) Dependently typed functional programs and their proofs, Ph.D. thesis, University of Edinburgh.Google Scholar
Nguyen, M. T., Giesl, J., Schneider-Kamp, P. and De Schreye, D. (2007) Termination Analysis of Logic Programs based on Dependency Graphs. In: King, A. (ed.) Logic-Based Program Synthesis and Transformation: Proceedings of LOPSTR'07. Springer-Verlag Lecture Notes in Computer Science 49158–22.Google Scholar
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.Google Scholar
Paulin-Mohring, C. (1989) Extracting Fω's Programs from Proofs in the Calculus of Constructions. Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages – POPL'89, ACM 89–104.Google Scholar
Paulin-Mohring, C. (1993) Inductive Definitions in the System Coq – Rules and Properties. In: Bezem, M. and Groote, J. (eds.) Typed Lambda Calculi and Applications: Proceedings of TLCA'93. Springer-Verlag Lecture Notes in Computer Science 664328–345.CrossRefGoogle Scholar
Peyton-Jones, S. (ed.) (2003) Haskell 98 Language and Libraries, The revised report, Cambridge University Press.Google Scholar
Saïbi, A. (1997) Typing algorithm in type theory with inheritance. Proceedings of the 24th Annual ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages – POPL'97, ACM 292–301.Google Scholar
Schneider-Kamp, P., Thiemann, R., Annov, E., Codish, M. and Giesl, J. (2007) Proving Termination using Recursive Path Orders and SAT Solving. In: Konev, B. and Wolter, F. (eds.) Frontiers of Combining Systems: Proceedings of FROCOS'07. Springer-Verlag Lecture Notes in Computer Science 4720267–282.CrossRefGoogle Scholar
Schneider-Kamp, P., Giesl, J., Serebrenik, A. and Thiemann, R. (2009) Automated Termination Proofs for Logic Programs by Term Rewriting. ACM Transactions on Computational Logic 11 (1)1–52.CrossRefGoogle Scholar
Sozeau, M. (2007) PROGRAM-ing Finger trees in Coq. Proceedings of ICFP'07. SIGPLAN Notices 42 (9).CrossRefGoogle Scholar
Sozeau, M. and Oury, N. (2008) First-class type classes. In: Mohamed, O. A., Muñoz, C. and Tahar, S. (eds.) Proceedings 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008). Springer-Verlag Lecture Notes in Computer Science 5170278–293.CrossRefGoogle Scholar
Sternagel, C. and Middeldorp, A. (2008) Root labeling. In: Voronkov, A. (ed.) Rewriting Techniques and Applications: Proceedings of RTA'08. Springer-Verlag Lecture Notes in Computer Science 5117336–350.CrossRefGoogle Scholar
Sternagel, C. and Thiemann, R. (2010) Certified Subterm Criterion and Certified Usable Rules. In: Lynch, C. (ed.) Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA '10). Leibniz International Proceedings in Informatics 6 325–340.Google Scholar
Sternagel, C., Thiemann, R., Winkler, S. and Zankl, H. (2010) CeTA.Google Scholar
Streicher, T. (1993) Investigations into Intensional Type Theory, Habilitation Thesis, Technical report, Ludwig-Maximilians-Universität München, Germany.Google Scholar
Strub, P.-Y. (2010a) Coq modulo theory. In: Dawar, A. and Veith, H. (eds.) Computer Science Logic: Proceedings of CSL'10. Springer-Verlag Lecture Notes in Computer Science 6247529–543.CrossRefGoogle Scholar
Strub, P.-Y. (2010b) Coq modulo theories. (Available at http://pierre-yves.strub.nu/research/coqmt/.)CrossRefGoogle Scholar
TeReSe (2003) Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science 55, Cambridge University Press.Google Scholar
Thiemann, R. and Sternagel, C. (2009) Certification of Termination Proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C. and Wenzel, M. (eds.) Proceedings 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009). Springer-Verlag Lecture Notes in Computer Science 5674452–468.CrossRefGoogle Scholar
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.)Google Scholar
Walukiewicz-Chrząszcz, D. and Chrząszcz, J. (2008) Consistency and completeness of rewriting in the Calculus of Constructions. Logical Methods in Computer Science 4 (3:8)1–20.Google Scholar
Werner, B. (1994) Une Théorie des Constructions Inductives, Ph.D. thesis, Université Paris VII.Google Scholar
Zantema, H. (1995) Termination of Term Rewriting by Semantic Labelling. Fundamenta Informaticae 24 89–105.CrossRefGoogle Scholar