Data refinement in Isabelle/HOL
From MaRDI portal
Recommendations
Cited in
(37)- Aligning concepts across proof assistant libraries
- A verified ODE solver and the Lorenz attractor
- Fast machine words in Isabelle/HOL
- A generic and executable formalization of signature-based Gröbner basis algorithms
- Isabelle's metalogic: formalization and proof checker
- A formalization and proof checker for Isabelle's metalogic
- A verified decision procedure for orders in Isabelle/HOL
- Traits: correctness-by-construction for free
- From LCF to Isabelle/HOL
- A verified implementation of algebraic numbers in Isabelle/HOL
- Formally verified certificate checkers for hardest-to-round computation
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Automating change of representation for proofs in discrete mathematics (extended version)
- Automatic refinement to efficient data structures: a comparison of two approaches
- From Sets to Bits in Coq
- Automatic functional correctness proofs for functional search trees
- Algebraic numbers in Isabelle/HOL
- Applying data refinement for monadic programs to Hopcroft's algorithm
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Deriving comparators and show functions in Isabelle/HOL
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
- Formalization and execution of linear algebra: from theorems to algorithms
- Code generation via higher-order rewrite systems
- Trustworthy Graph Algorithms (Invited Talk)
- Light-weight containers for Isabelle: efficient, extensible, nestable
- 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
- Matching concepts across HOL libraries
- The Isabelle collections framework
- scientific article; zbMATH DE number 7649971 (Why is no real title available?)
- Efficient verified (UN)SAT certificate checking
- Flexible Correct-by-Construction Programming
- Isomorphic data type transformations
- Nondeterministic asynchronous dataflow in Isabelle/HOL
- Building program construction and verification tools from algebraic principles
- Some proofs of data refinement
- Data refinement and singleton failures refinement are not equivalent
This page was built for publication: Data refinement in Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5327339)
