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. © 2013 Springer-Verlag.
CITATION STYLE
Haftmann, F., Krauss, A., Kunčar, O., & Nipkow, T. (2013). Data refinement in Isabelle/HOL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7998 LNCS, pp. 100–115). https://doi.org/10.1007/978-3-642-39634-2_10
Mendeley helps you to discover research relevant for your work.