Data refinement in Isabelle/HOL

DOI10.1007/978-3-642-39634-2_10MaRDI QIDQ5327339zbMATH OpenOpenAlexFDO

Authors Florian Haftmann, Alexander Krauss, Ondřej Kunčar, Tobias Nipkow

Publication date 7 August 2013

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-39634-2_10

Mathematics Subject Classification ID

Recommendations

• Automatic Data Refinement
• Automatic refinement to efficient data structures: a comparison of two approaches
• Applying data refinement for monadic programs to Hopcroft's algorithm
• Refinement to Imperative/HOL
• Refinement to imperative HOL

Cited in

(36)

• From Sets to Bits in Coq
• Flexible Correct-by-Construction Programming
• Algebraic numbers in Isabelle/HOL
• A verified implementation of algebraic numbers in Isabelle/HOL
• Deriving comparators and show functions 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
• Automatic functional correctness proofs for functional search trees
• The Isabelle collections framework
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Aligning concepts across proof assistant libraries
• Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
• A generic and executable formalization of signature-based Gröbner basis algorithms
• Efficient verified (UN)SAT certificate checking
• Fast machine words in Isabelle/HOL
• Isomorphic data type transformations
• Applying data refinement for monadic programs to Hopcroft's algorithm
• Matching concepts across HOL libraries
• Building program construction and verification tools from algebraic principles
• Automating change of representation for proofs in discrete mathematics (extended version)
• A verified decision procedure for orders in Isabelle/HOL
• Trustworthy Graph Algorithms (Invited Talk)
• Data refinement and singleton failures refinement are not equivalent
• A verified ODE solver and the Lorenz attractor
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)
• Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
• Formalization and execution of linear algebra: from theorems to algorithms
• Traits: correctness-by-construction for free
• Verified decision procedures for MSO on words based on derivatives of regular expressions
• Isabelle's metalogic: formalization and proof checker
• A formalization and proof checker for Isabelle's metalogic
• Some proofs of data refinement
• From LCF to Isabelle/HOL
• Formally verified certificate checkers for hardest-to-round computation
• Automatic refinement to efficient data structures: a comparison of two approaches
• Code generation via higher-order rewrite systems
• Light-weight containers for Isabelle: efficient, extensible, nestable

Describes a project that uses

Uses Software

• Isabelle/HOL

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)