### 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.

### License

BSD License

### History

March 5, 2018
  add two application examples: depth-first search and 2SAT (revision e5e1a1da2411)
July 8, 2014
  add support for going from partial functions to mappings (revision 7a6fc957e8ed)
September 20, 2013
  provide generators for canonical type class instantiations (revision 159f4401f4a8 by René Thiemann)
July 11, 2013
  add pretty printing for sets (revision 7f3f52c5f5fa)

### Topics

- Computer science/Data structures

### Session Containers

- Containers_Auxiliary
- Card_Datatype
- List_Fusion
- Lexicographic_Order
- Extend_Partial_Order
- Set_Linorder
- Containers_Generator
- Collection_Order
- List_Proper_Interval
- Collection_Eq
- Collection_Enum
- Equal
- RBT_ext
- RBT_Mapping2
- AssocList
- DList_Set
- RBT_Set2
- Closure_Set
- Set_Impl
- Mapping_Impl
- Map_To_Mapping
- Containers
- Compatibility_Containers_Regular_Sets
- Containers_Userguide
- Card_Datatype_Ex
- Map_To_Mapping_Ex
- TwoSat_Ex
- Containers_DFS_Ex
- Containers_TwoSat_Ex

### Session Containers-Benchmarks

- Benchmark_Bool
- Benchmark_Comparison
- Benchmark_LC
- Benchmark_Default
- Benchmark_ICF
- Benchmark_RBT
- Benchmark_Set
- Benchmark_Set_Default
- Benchmark_Set_LC
- Clauses

### Depends on

- Automatic Data Refinement
- Collections Framework
- Deriving class instances for datatypes
- Finger Trees
- Regular Sets and Expressions
- Trie

### Used by

- A Formal CHERI-C Memory Model
- Verified Complete Test Strategies for Finite State Machines
- First-Order Query Evaluation
- Multi-Head Monitoring of Metric Dynamic Logic
- AI Planning Languages Semantics
- Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic
- Polynomial Factorization
- Collections Framework

### Auto-related entries

- A Verified Code Generator from Isabelle/HOL to CakeML
- XML
- Imperative Insertion Sort
- Native Word

## Cite

×

Containers-AFP

    @article{Containers-AFP,
      author  = {Andreas Lochbihler},
      title   = {Light-weight Containers},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2013},
      note    = {\url{https://isa-afp.org/entries/Containers.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Apr 23, 2013 : Isabelle2013