CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
From MaRDI portal
Publication:3094178
DOI10.1017/S0960129511000120zbMath1223.68101arXiv1202.6473OpenAlexW2117247884MaRDI QIDQ3094178
Adam Koprowski, Frédéric Blanqui
Publication date: 21 October 2011
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1202.6473
Related Items
Analyzing program termination and complexity automatically with \textsf{AProVE}, Automatically proving termination and memory safety for programs with pointer arithmetic, How to get more out of your oracles, Formally proving size optimality of sorting networks, Integration of multiple formal matrix models in Coq, A Lambda-Free Higher-Order Recursive Path Order, Mechanically certifying formula-based Noetherian induction reasoning, Syntactic soundness proof of a type-and-capability system with hidden state, A framework for developing stand-alone certifiers, Unnamed Item, Termination of Isabelle Functions via Termination of Rewriting, Multi-dimensional interpretations for termination of term rewriting, CoLoR, A Framework for Certified Self-Stabilization, Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems, Formally verifying the solution to the Boolean Pythagorean triples problem, Tuple interpretations for termination of term rewriting
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Orderings for term-rewriting systems
- Coq formalization of the higher-order recursive path ordering
- Mechanically proving termination using polynomial interpretations
- An effective proof of the well-foundedness of the multiset path ordering
- Tyrolean termination tool: techniques and features
- Mechanizing and improving dependency pairs
- Matrix interpretations for proving termination of term rewriting
- Analysing the implicit complexity of programs.
- Theorem proving modulo
- Modular termination proofs for rewriting using dependency pairs
- Termination of term rewriting using dependency pairs
- Automating the dependency pair method
- Automated termination proofs for logic programs by term rewriting
- Certification of Termination Proofs Using CeTA
- Arctic Termination ...Below Zero
- Root-Labeling
- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
- Certification of Automated Termination Proofs
- Proving Termination Using Recursive Path Orders and SAT Solving
- Certified Higher-Order Recursive Path Ordering
- Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
- Automated Complexity Analysis Based on the Dependency Pair Method
- Certifying a Termination Criterion Based on Graphs, without Graphs
- First-Class Type Classes
- Code Generation via Higher-Order Rewrite Systems
- Coq Modulo Theory
- Building Decision Procedures in the Calculus of Inductive Constructions
- Certified Size-Change Termination
- SAT Solving for Termination Analysis with Polynomial Interpretations
- Modularity of strong normalization in the algebraic-λ-cube
- Proof normalization modulo
- Definitions by rewriting in the Calculus of Constructions
- Certification of Proving Termination of Term Rewriting by Matrix Interpretations
- An Efficient Coq Tactic for Deciding Kleene Algebras
- Consistency and Completeness of Rewriting in the Calculus of Constructions
