Light-weight Containers

Title:	Light-weight Containers
Author:	Andreas Lochbihler
Contributor:	René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
Submission date:	2013-04-15
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.
Change history:	[2013-07-11]: add pretty printing for sets (revision 7f3f52c5f5fa) [2013-09-20]: provide generators for canonical type class instantiations (revision 159f4401f4a8 by René Thiemann) [2014-07-08]: add support for going from partial functions to mappings (revision 7a6fc957e8ed) [2018-03-05]: add two application examples: depth-first search and 2SAT (revision e5e1a1da2411)
BibTeX:	@article{Containers-AFP, author = {Andreas Lochbihler}, title = {Light-weight Containers}, journal = {Archive of Formal Proofs}, month = apr, year = 2013, note = {\url{http://isa-afp.org/entries/Containers.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Automatic_Refinement, Collections, Deriving, Finger-Trees, Regular-Sets
Used by:	MFOTL_Monitor
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Proof outline
Proof document

Browse theories

Download this entry