Code generation via higher-order rewrite systems
From MaRDI portal
Recommendations
Cited in
(61)- CoSMed: a confidentiality-verified social media platform
- Verified iptables firewall analysis and verification
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
- CoCon: a conference management system with formally verified document confidentiality
- Isabelle's metalogic: formalization and proof checker
- A formalization and proof checker for Isabelle's metalogic
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- From LCF to Isabelle/HOL
- Certified equational reasoning via ordered completion
- Proof pearl: A mechanized proof of GHC's mergesort
- Proving divide and conquer complexities in Isabelle/HOL
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Soundness and completeness proofs by coinductive methods
- Proof Pearl: regular expression equivalence and relation algebra
- Automatic refinement to efficient data structures: a comparison of two approaches
- Using rewriting techniques to produce code generators and proving them correct
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Translating Scala programs to Isabelle/HOL. System description
- CoSMed: a confidentiality-verified social media platform
- Formalizing the Edmonds-Karp algorithm
- Deriving comparators and show functions in Isabelle/HOL
- Pattern matches in HOL: a new representation and improved code generation
- Certifying confluence proofs via relative termination and rule labeling
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Comprehending Isabelle/HOL’s Consistency
- Verified synthesis of knowledge-based programs in finite synchronous environments
- Animating the formalised semantics of a Java-like language
- Verified efficient enumeration of plane graphs modulo isomorphism
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
- Automatic proof and disproof in Isabelle/HOL
- Turning Inductive into Equational Specifications
- Formalization and execution of linear algebra: from theorems to algorithms
- Verification and code generation for invariant diagrams in Isabelle
- Verified Root-Balanced Trees
- Trustworthy Graph Algorithms (Invited Talk)
- Programming and verifying a declarative first-order prover in Isabelle/HOL
- Reachability, confluence, and termination analysis with state-compatible automata
- Certifying dictionary construction in Isabelle/HOL
- A formal proof of the Kepler conjecture
- A framework for developing stand-alone certifiers
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
- Verified decision procedures for MSO on words based on derivatives of regular expressions
- Hipster: integrating theory exploration in a proof assistant
- Set theory or higher order logic to represent auction concepts in Isabelle?
- Partiality and recursion in interactive theorem provers -- an overview
- scientific article; zbMATH DE number 7649972 (Why is no real title available?)
- Efficient verified (UN)SAT certificate checking
- VeriMon: a formally verified monitoring tool
- Combining higher-order logic with set theory formalizations
- A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
- Gale-Shapley verified
- Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker
- Amortized complexity verified
- Certainty in formalising SMT-LIB for strings in Isabelle
- Derandomization with pseudorandomness
- Formally verified suffix array construction
- Fast, verified computation for HOL ITPs
- Nondeterministic asynchronous dataflow in Isabelle/HOL
This page was built for publication: Code generation via higher-order rewrite systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3558332)
