CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates. 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. 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.

References in zbMATH (referenced in 31 articles , 1 standard article )

Showing results 1 to 20 of 31.
Sorted by year (citations)

1 2 next

  1. Kokosiński, Zbigniew; Bała, Marcin: Solving graph partitioning problems with parallel metaheuristics (2018)
  2. Blanchette, Jasmin Christian; Waldmann, Uwe; Wand, Daniel: A lambda-free higher-order recursive path order (2017)
  3. Brockschmidt, Marc; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa: Certifying safety and termination proofs for integer transition systems (2017)
  4. Cruz-Filipe, Luís; Larsen, Kim S.; Schneider-Kamp, Peter: Formally proving size optimality of sorting networks (2017)
  5. Giesl, Jürgen; Aschermann, Cornelius; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René: Analyzing program termination and complexity automatically with \ssfAProVE (2017)
  6. Sternagel, Christian; Sternagel, Thomas: Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems (2017)
  7. Stratulat, Sorin: Mechanically certifying formula-based Noetherian induction reasoning (2017)
  8. Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius: Automatically proving termination and memory safety for programs with pointer arithmetic (2017)
  9. Altisen, Karine; Corbineau, Pierre; Devismes, Stéphane: A framework for certified self-stabilization (2016)
  10. Nagele, Julian; Middeldorp, Aart: Certification of classical confluence results for left-linear term rewrite systems (2016)
  11. Sternagel, Christian; Thiemann, René: A framework for developing stand-alone certifiers (2015)
  12. Pottier, François: Syntactic soundness proof of a type-and-capability system with hidden state (2013)
  13. Braibant, Thomas; Pous, Damien: Deciding Kleene algebras in Coq (2012)
  14. Blanqui, Frédéric; Koprowski, Adam: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates (2011)
  15. Gonthier, Georges: Point-free, set-free concrete linear algebra (2011)
  16. Krauss, Alexander; Sternagel, Christian; Thiemann, René; Fuhs, Carsten; Giesl, Jürgen: Termination of Isabelle functions via termination of rewriting (2011)
  17. Sternagel, Christian; Thiemann, René: Generalized and formalized uncurrying (2011)
  18. Galdino, André L.; Ayala-Rincón, Mauricio: A formalization of the Knuth-Bendix(-Huet) critical pair theorem (2010)
  19. Sternagel, Christian; Thiemann, René: Certified subterm criterion and certified usable rules (2010)
  20. Koprowski, Adam: Coq formalization of the higher-order recursive path ordering (2009)

1 2 next

Further publications can be found at: