HOME | DEUTSCH | IMPRESSUM | KIT

Journal Article: Light-weight Containers

[lochbihler13afp]Andreas Lochbihler, Light-weight Containers, Archive of Formal Proofs, April 2013. Formal proof development

Abstract

This development provides a framework for container types like sets and maps such that generated code implements these containers with different (efficient) data structures. Thanks to type classes and refinement during code generation, this light-weight approach can seamlessly replace Isabelle's default setup for code generation. Heuristics automatically pick one of the available data structures depending on the type of elements to be stored, but users can also choose on their own. The extensible design permits to add more implementations at any time. To support arbitrary nesting of sets, we define a linear order on sets based on a linear order of the elements and provide efficient implementations. It even allows to compare complements with non-complements.

Download

  [Link]

BibTeX

Authors at the institute

Former Staff Member
Dr. rer. nat. Andreas Lochbihler

Projects

Project
Quis-Custodiet