The following pages link to CoLoR (Q21785):
Displayed 38 items.
- Mechanically certifying formula-based Noetherian induction reasoning (Q507366) (← links)
- A framework for developing stand-alone certifiers (Q530847) (← links)
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem (Q616850) (← links)
- Coq formalization of the higher-order recursive path ordering (Q843949) (← links)
- An effective proof of the well-foundedness of the multiset path ordering (Q857884) (← links)
- Formally proving size optimality of sorting networks (Q1694569) (← links)
- Multi-dimensional interpretations for termination of term rewriting (Q2055861) (← links)
- Tuple interpretations for termination of term rewriting (Q2102931) (← links)
- Formally verifying the solution to the Boolean Pythagorean triples problem (Q2323449) (← links)
- Analyzing program termination and complexity automatically with \textsf{AProVE} (Q2362493) (← links)
- Automatically proving termination and memory safety for programs with pointer arithmetic (Q2362494) (← links)
- Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems (Q2405266) (← links)
- Certifying safety and termination proofs for integer transition systems (Q2405269) (← links)
- A Framework for Certified Self-Stabilization (Q2827460) (← links)
- Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems (Q2829264) (← links)
- Deciding Kleene Algebras in Coq (Q2881083) (← links)
- A Lambda-Free Higher-Order Recursive Path Order (Q2988386) (← links)
- (Q3077191) (← links)
- Point-Free, Set-Free Concrete Linear Algebra (Q3088000) (← links)
- Termination of Isabelle Functions via Termination of Rewriting (Q3088004) (← links)
- Generalized and Formalized Uncurrying (Q3172898) (← links)
- Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence (Q3183536) (← links)
- Certification of Termination Proofs Using CeTA (Q3183545) (← links)
- Proving Termination of Programs Automatically with AProVE (Q3192189) (← links)
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant (Q3434629) (← links)
- (Q3497624) (← links)
- Certifying a Termination Criterion Based on Graphs, without Graphs (Q3543658) (← links)
- Modeling Permutations in Coq for Coccinelle (Q3608821) (← links)
- Automatic Termination (Q3636815) (← links)
- Solving Graph Partitioning Problems with Parallel Metaheuristics (Q4609771) (← links)
- Syntactic soundness proof of a type-and-capability system with hidden state (Q4912884) (← links)
- (Q5111307) (← links)
- A PVS Theory for Term Rewriting Systems (Q5178962) (← links)
- (Q5277883) (← links)
- CERTIFIED SUBTERM CRITERION AND CERTIFIED USABLE RULES (Q5389153) (← links)
- Certification of Proving Termination of Term Rewriting by Matrix Interpretations (Q5448658) (← links)
- An Efficient Coq Tactic for Deciding Kleene Algebras (Q5747648) (← links)
- Preface (Q5894305) (← links)