Conference Papers: Light-weight containers for Isabelle: efficient, extensible, nestable

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.