| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
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. |
| BibTeX: |
@article{Automatic_Refinement-AFP,
author = {Peter Lammich},
title = {Automatic Data Refinement},
journal = {Archive of Formal Proofs},
month = oct,
year = 2013,
note = {\url{http://isa-afp.org/entries/Automatic_Refinement.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Used by: | Containers, Dict_Construction, IP_Addresses, JinjaThreads, Network_Security_Policy_Verification, Refine_Monadic, ROBDD, Separation_Logic_Imperative_HOL, UpDown_Scheme |
| 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. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |