CoLoR

swMATH9806MaRDI QIDQ21785FDOQ21785

Author name not available (Why is that?)

Described by source

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

Cited In (38)

• Formally verifying the solution to the Boolean Pythagorean triples problem
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Tuple interpretations for termination of term rewriting
• A framework for developing stand-alone certifiers
• Multi-dimensional interpretations for termination of term rewriting
• Title not available (Why is that?)
• Certification of Proving Termination of Term Rewriting by Matrix Interpretations
• Automatic Termination
• An Efficient Coq Tactic for Deciding Kleene Algebras
• Title not available (Why is that?)
• Coq formalization of the higher-order recursive path ordering
• An effective proof of the well-foundedness of the multiset path ordering
• Termination of Isabelle Functions via Termination of Rewriting
• Certification of Termination Proofs Using CeTA
• Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence
• Solving Graph Partitioning Problems with Parallel Metaheuristics
• Generalized and Formalized Uncurrying
• Title not available (Why is that?)
• Modeling Permutations in Coq for Coccinelle
• Certifying a Termination Criterion Based on Graphs, without Graphs
• Title not available (Why is that?)
• A PVS Theory for Term Rewriting Systems
• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• A formalization of the Knuth-Bendix(-Huet) critical pair theorem
• CERTIFIED SUBTERM CRITERION AND CERTIFIED USABLE RULES
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems
• Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems
• Certifying safety and termination proofs for integer transition systems
• A Framework for Certified Self-Stabilization
• Proving Termination of Programs Automatically with AProVE
• Syntactic soundness proof of a type-and-capability system with hidden state
• A Lambda-Free Higher-Order Recursive Path Order
• Preface
• Formally proving size optimality of sorting networks
• Mechanically certifying formula-based Noetherian induction reasoning
• Point-Free, Set-Free Concrete Linear Algebra
• Deciding Kleene algebras in \texttt{Coq}

This page was built for software: CoLoR