Pages that link to "Item:Q3558332"
From MaRDI portal
The following pages link to Code Generation via Higher-Order Rewrite Systems (Q3558332):
Displayed 49 items.
- Verification and code generation for invariant diagrams in Isabelle (Q478381) (← links)
- Reachability, confluence, and termination analysis with state-compatible automata (Q515687) (← links)
- A framework for developing stand-alone certifiers (Q530847) (← links)
- Amortized complexity verified (Q670702) (← links)
- CoSMed: a confidentiality-verified social media platform (Q1663221) (← links)
- Verified iptables firewall analysis and verification (Q1663231) (← links)
- A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (Q1722647) (← links)
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (Q1725844) (← links)
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm (Q1984794) (← links)
- CoCon: a conference management system with formally verified document confidentiality (Q2031419) (← links)
- Isabelle's metalogic: formalization and proof checker (Q2055847) (← links)
- A formalization and proof checker for Isabelle's metalogic (Q2108191) (← links)
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL (Q2209537) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Certified equational reasoning via ordered completion (Q2305436) (← links)
- Proof pearl: A mechanized proof of GHC's mergesort (Q2351394) (← links)
- Proving divide and conquer complexities in Isabelle/HOL (Q2362108) (← links)
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (Q2362109) (← links)
- Soundness and completeness proofs by coinductive methods (Q2362498) (← links)
- Proof Pearl: regular expression equivalence and relation algebra (Q2392416) (← links)
- Automatic refinement to efficient data structures: a comparison of two approaches (Q2417948) (← links)
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Q2817909) (← links)
- Translating Scala Programs to Isabelle/HOL (Q2817953) (← links)
- CoSMed: A Confidentiality-Verified Social Media Platform (Q2829248) (← links)
- Formalizing the Edmonds-Karp Algorithm (Q2829260) (← links)
- Deriving Comparators and Show Functions in Isabelle/HOL (Q2945654) (← links)
- (Q2985126) (← links)
- Friends with Benefits (Q2988636) (← links)
- Comprehending Isabelle/HOL’s Consistency (Q2988665) (← links)
- Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments (Q3087999) (← links)
- Animating the Formalised Semantics of a Java-Like Language (Q3088008) (← links)
- Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism (Q3088012) (← links)
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates (Q3094178) (← links)
- Automatic Proof and Disproof in Isabelle/HOL (Q3172879) (← links)
- Formalization and Execution of Linear Algebra: From Theorems to Algorithms (Q3453644) (← links)
- Verified Root-Balanced Trees (Q5056001) (← links)
- Trustworthy Graph Algorithms (Invited Talk) (Q5092359) (← links)
- Programming and verifying a declarative first-order prover in Isabelle/HOL (Q5145439) (← links)
- A FORMAL PROOF OF THE KEPLER CONJECTURE (Q5280247) (← links)
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm (Q5371950) (← links)
- Verified decision procedures for MSO on words based on derivatives of regular expressions (Q5371957) (← links)
- Hipster: Integrating Theory Exploration in a Proof Assistant (Q5495917) (← links)
- Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle? (Q5495927) (← links)
- Partiality and recursion in interactive theorem provers – an overview (Q5741556) (← links)
- (Q5875432) (← links)
- Efficient verified (UN)SAT certificate checking (Q5919480) (← links)
- VeriMon: a formally verified monitoring tool (Q6109465) (← links)
- Combining higher-order logic with set theory formalizations (Q6161232) (← links)