The following pages link to CeTA (Q18676):
Displayed 46 items.
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Proving termination by dependency pairs and inductive theorem proving (Q438537) (← links)
- Reachability, confluence, and termination analysis with state-compatible automata (Q515687) (← links)
- A framework for developing stand-alone certifiers (Q530847) (← links)
- Proof certificates for equality reasoning (Q1744408) (← links)
- Fast machine words in Isabelle/HOL (Q1791180) (← links)
- Multi-dimensional interpretations for termination of term rewriting (Q2055861) (← links)
- Tuple interpretations for termination of term rewriting (Q2102931) (← links)
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL (Q2209537) (← links)
- A Perron-Frobenius theorem for deciding matrix growth (Q2239274) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- A verified implementation of algebraic numbers in Isabelle/HOL (Q2303244) (← links)
- A framework for the verification of certifying computations (Q2351144) (← links)
- Proof pearl: A mechanized proof of GHC's mergesort (Q2351394) (← links)
- Formalizing complex plane geometry (Q2354913) (← 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)
- Proof Pearl: regular expression equivalence and relation algebra (Q2392416) (← links)
- CSI: new evidence -- a progress report (Q2405264) (← 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)
- Automatic refinement to efficient data structures: a comparison of two approaches (Q2417948) (← links)
- Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems (Q2829264) (← links)
- KBCV – Knuth-Bendix Completion Visualizer (Q2908523) (← links)
- Stream Fusion for Isabelle’s Code Generator (Q2945639) (← links)
- Deriving Comparators and Show Functions in Isabelle/HOL (Q2945654) (← links)
- (Q2958390) (← links)
- (Q2985126) (← links)
- A Lambda-Free Higher-Order Recursive Path Order (Q2988386) (← links)
- Termination of Isabelle Functions via Termination of Rewriting (Q3088004) (← links)
- Animating the Formalised Semantics of a Java-Like Language (Q3088008) (← links)
- A Decision Procedure for Regular Expression Equivalence in Type Theory (Q3100207) (← links)
- Generalized and Formalized Uncurrying (Q3172898) (← links)
- Proving Termination of Programs Automatically with AProVE (Q3192189) (← links)
- A Mechanized Proof of Higman’s Lemma by Open Induction (Q3295156) (← links)
- Code Generation via Higher-Order Rewrite Systems (Q3558332) (← links)
- (Q5232901) (← links)
- (Q5277869) (← links)
- (Q5277883) (← links)
- (Q5277884) (← links)
- (Q5278394) (← links)
- (Q5389090) (← links)
- (Q5389153) (← links)
- Modular Complexity Analysis for Term Rewriting (Q5408194) (← links)
- Formalizing Bachmair and Ganzinger's ordered resolution prover (Q5916290) (← links)
- Formalizing Bachmair and Ganzinger's ordered resolution prover (Q5919011) (← links)