HOME | DEUTSCH | IMPRESSUM | KIT

Conference Papers: The Isabelle Collections Framework

[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

  [PDF]   [DOI]

Original article available at springerlink.com.

BibTeX

Authors at the institute

Former Staff Member
Dr. rer. nat. Andreas Lochbihler

Projects

Project
Quis-Custodiet