Data Refinement in Isabelle/HOL
From MaRDI portal
Publication:5327339
DOI10.1007/978-3-642-39634-2_10zbMath1317.68212OpenAlexW1713610MaRDI QIDQ5327339
Tobias Nipkow, Alexander Krauss, Ondřej Kunčar, Florian Haftmann
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (26)
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) ⋮ Formalization and Execution of Linear Algebra: From Theorems to Algorithms ⋮ Aligning concepts across proof assistant libraries ⋮ A verified decision procedure for orders in Isabelle/HOL ⋮ Traits: correctness-by-construction for free ⋮ A verified ODE solver and the Lorenz attractor ⋮ Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL ⋮ Automatic refinement to efficient data structures: a comparison of two approaches ⋮ Flexible Correct-by-Construction Programming ⋮ Unnamed Item ⋮ Verified decision procedures for MSO on words based on derivatives of regular expressions ⋮ Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm ⋮ From LCF to Isabelle/HOL ⋮ A generic and executable formalization of signature-based Gröbner basis algorithms ⋮ From Sets to Bits in Coq ⋮ Building program construction and verification tools from algebraic principles ⋮ Efficient verified (UN)SAT certificate checking ⋮ A verified implementation of algebraic numbers in Isabelle/HOL ⋮ Isabelle's metalogic: formalization and proof checker ⋮ Trustworthy Graph Algorithms (Invited Talk) ⋮ Automatic Functional Correctness Proofs for Functional Search Trees ⋮ Algebraic Numbers in Isabelle/HOL ⋮ Matching Concepts across HOL Libraries ⋮ A formalization and proof checker for Isabelle's metalogic ⋮ Formally verified certificate checkers for hardest-to-round computation
Uses Software
This page was built for publication: Data Refinement in Isabelle/HOL
