Abstract
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. © 2013 Springer-Verlag.
Cite
CITATION STYLE
Lochbihler, A. (2013). Light-weight containers for Isabelle: Efficient, extensible, nestable. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7998 LNCS, pp. 116–132). https://doi.org/10.1007/978-3-642-39634-2_11
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
