HOME | ENGLISH | IMPRESSUM | KIT

Konferenzartikel: Light-weight containers for Isabelle: efficient, extensible, nestable

[lochbihler13itp]Andreas Lochbihler, Light-weight containers for Isabelle: efficient, extensible, nestable, Interactive Theorem Proving, pp. 116--132, Springer, 2013.

Zusammenfassung

In Isabelle/HOL, we develop an approach to efficiently implement container types such as sets and maps in generated code. Thanks to type classes and refinement during code generation, our light-weight framework is flexible, extensible, and easy to use. To support arbitrary nesting of containers, we devise an efficient linear order on sets that can even compare complements and non-complements. Our evaluation shows that it is both efficient and usable.

Download

  [PDF]   [DOI]

Original article available at springerlink.com.

BibTeX

Institutsinterne Autoren

Ehemalige Mitarbeiter
Dr. rer. nat. Andreas Lochbihler

Projekte

Projekt
Quis-Custodiet