CoLoR

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 36 articles , 1 standard article )

Showing results 1 to 20 of 36.
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 \textsfAProVE (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. Nagele, Julian; Felgenhauer, Bertram; Middeldorp, Aart: Improving automatic confluence analysis of rewrite systems by redundant rules (2015)
  12. Sternagel, Christian; Thiemann, René: A framework for developing stand-alone certifiers (2015)
  13. Giesl, Jürgen; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René: Proving termination of programs automatically with AProVE (2014)
  14. Pottier, François: Syntactic soundness proof of a type-and-capability system with hidden state (2013)
  15. Braibant, Thomas; Pous, Damien: Deciding Kleene algebras in \textttCoq (2012)
  16. Christian Sternagel, René Thiemann, Sarah Winkler, Harald Zankl: CeTA - A Tool for Certified Termination Analysis (2012) arXiv
  17. 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)
  18. Gonthier, Georges: Point-free, set-free concrete linear algebra (2011)
  19. Huet, Gérard: Preface to the special issue: Interactive theorem proving and the formalization of mathematics (2011)
  20. Krauss, Alexander; Sternagel, Christian; Thiemann, René; Fuhs, Carsten; Giesl, Jürgen: Termination of Isabelle functions via termination of rewriting (2011)

1 2 next


Further publications can be found at: http://color.inria.fr/biblio.html