[lammich10itp] | Peter Lammich, Andreas Lochbihler, The Isabelle Collections Framework, pp. 339--354, Springer, July 2010.
|
Abstract
The Isabelle Collections Framework (ICF) provides a unified framework
for using verified collection data structures in Isabelle/HOL formalizations
and generating efficient functional code in ML, Haskell, and OCaml.
Thanks to its modularity, it is easily extensible and supports switching
to different data structures any time. For good integration with
applications, a data refinement approach separates the correctness
proofs from implementation details. The generated code based on the
ICF lies in better complexity classes than the one that uses Isabelle's
default setup (logarithmic vs. linear time). In a case study with
tree automata, we demonstrate that the ICF is easy to use and efficient:
An ICF based, verified tree automata library outperforms the unverified
Timbuk/Taml library by a factor of 14.
Download
Original article available at springerlink.com.
BibTeX
Authors at the institute
Projects