CeTA

swMATH6584MaRDI QIDQ18676FDOQ18676

Author name not available (Why is that?)

Described by source

• Certification of Termination Proofs Using CeTA

Cited In (46)

• Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
• Stream Fusion for Isabelle’s Code Generator
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• A Decision Procedure for Regular Expression Equivalence in Type Theory
• Tuple interpretations for termination of term rewriting
• A framework for developing stand-alone certifiers
• Multi-dimensional interpretations for termination of term rewriting
• CSI: new evidence -- a progress report
• Modular and Certified Semantic Labeling and Unlabeling
• Title not available (Why is that?)
• A Mechanized Proof of Higman’s Lemma by Open Induction
• Certified Rule Labeling
• A verified implementation of algebraic numbers in Isabelle/HOL
• Title not available (Why is that?)
• AC Dependency Pairs Revisited
• Animating the Formalised Semantics of a Java-Like Language
• Termination of Isabelle Functions via Termination of Rewriting
• Proof pearl: A mechanized proof of GHC's mergesort
• Code Generation via Higher-Order Rewrite Systems
• Fast machine words in Isabelle/HOL
• A framework for the verification of certifying computations
• Proving termination by dependency pairs and inductive theorem proving
• Generalized and Formalized Uncurrying
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Title not available (Why is that?)
• Deriving Comparators and Show Functions in Isabelle/HOL
• Title not available (Why is that?)
• Proof Pearl: regular expression equivalence and relation algebra
• Formalizing complex plane geometry
• A learning-based fact selector for Isabelle/HOL
• A Perron-Frobenius theorem for deciding matrix growth
• CERTIFIED SUBTERM CRITERION AND CERTIFIED USABLE RULES
• Automatically proving termination and memory safety for programs with pointer arithmetic
• From LCF to Isabelle/HOL
• Modular Complexity Analysis for Term Rewriting
• 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
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Proving Termination of Programs Automatically with AProVE
• A Lambda-Free Higher-Order Recursive Path Order
• Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
• KBCV – Knuth-Bendix Completion Visualizer
• Automatic refinement to efficient data structures: a comparison of two approaches
• Proof certificates for equality reasoning
• Reachability, confluence, and termination analysis with state-compatible automata

This page was built for software: CeTA