Automatic Data Refinement


Title: Automatic Data Refinement
Author: Peter Lammich
Submission date: 2013-10-02
Abstract: We present the Autoref tool for Isabelle/HOL, which automatically refines algorithms specified over abstract concepts like maps and sets to algorithms over concrete implementations like red-black-trees, and produces a refinement theorem. It is based on ideas borrowed from relational parametricity due to Reynolds and Wadler. The tool allows for rapid prototyping of verified, executable algorithms. Moreover, it can be configured to fine-tune the result to the user~s needs. Our tool is able to automatically instantiate generic algorithms, which greatly simplifies the implementation of executable data structures.

This AFP-entry provides the basic tool, which is then used by the Refinement and Collection Framework to provide automatic data refinement for the nondeterminism monad and various collection datastructures.

  author  = {Peter Lammich},
  title   = {Automatic Data Refinement},
  journal = {Archive of Formal Proofs},
  month   = oct,
  year    = 2013,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Used by: Collections, DFS_Framework, EdmondsKarp_Maxflow, IP_Addresses, Iptables_Semantics, LOFT, Network_Security_Policy_Verification, Ordinary_Differential_Equations, ROBDD, Refine_Imperative_HOL, Refine_Monadic, Separation_Logic_Imperative_HOL, Tree-Automata
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.