Data Refinement in Isabelle/HOL
The paper shows how the code generator of Isabelle/HOL supports data
refinement, i.e., providing efficient code for operations on abstract
types, e.g., sets or numbers. This allows all tools that employ code
generation, e.g., Quickcheck or proof by evaluation, to compute with
these abstract types. At the core is an extension of the code
generator to deal with data type invariants. In order to automate the
process of setting up specific data refinements, two packages for
transferring definitions and theorems between types are exploited.
pdf
BibTeX:
@inproceedings{HaftmannKKN-ITP13,
author={Florian Haftmann and Alexander Krauss and Ond\v{r}ej Kun\v{c}ar and Tobias Nipkow},
title={Data Refinement in Isabelle/HOL},
booktitle={Interactive Theorem Proving (ITP 2013)},
editor={S. Blazy and C. Paulin-Mohring and D. Pichardie},
publisher=Springer,series=LNCS,volume={7998},pages={100-115},year=2013}