Collections Framework

Peter Lammich 🌐 with contributions from Andreas Lochbihler 🌐 and Thomas Tuerk

November 25, 2009


This development provides an efficient, extensible, machine checked collections framework. The library adopts the concepts of interface, implementation and generic algorithm from object-oriented programming and implements them in Isabelle/HOL. The framework features the use of data refinement techniques to refine an abstract specification (using high-level concepts like sets) to a more concrete implementation (using collection datastructures, like red-black-trees). The code-generator of Isabelle/HOL can be used to generate efficient code.


BSD License


April 25, 2012
New iterator foundation by Tuerk. Various maintenance changes.
October 10, 2011
SetSpec: Added operations: sng, isSng, bexists, size_abort, diff, filter, iterate_rule_insertP MapSpec: Added operations: sng, isSng, iterate_rule_insertP, bexists, size, size_abort, restrict, map_image_filter, map_value_image_filter Some maintenance changes
December 1, 2010
New Interfaces: Priority Queues, Annotated Lists. Implemented by finger trees, (skew) binomial queues.
October 8, 2010
New Interfaces: OrderedSet, OrderedMap, List. Fifo now implements list-interface: Function names changed: put/get --> enqueue/dequeue. New Implementations: ArrayList, ArrayHashMap, ArrayHashSet, TrieMap, TrieSet. Invariant-free datastructures: Invariant implicitely hidden in typedef. Record-interfaces: All operations of an interface encapsulated as record. Examples moved to examples subdirectory.


Related publications

Session Collections

Session Collections_Examples