Modular Finite Maps over Ordered Types

This project contains several implementations of finite maps, including implementations based on AVL trees and red-black trees. The finite maps are parameterized on arbitrary ordered types using Coq functors. This is an updated version of the Coq Stdlib's FMaps that is meant to complement the Stdlib's MSet library.

Meta

• Author(s):
  • Pierre Letouzey (initial)
  • Andrew W. Appel
• Coq-community maintainer(s):
  • Pierre Letouzey (@letouzey)
  • Karl Palmskog (@palmskog)
• License: GNU Lesser General Public License v2.1 only
• Compatible Coq versions: 8.14 and later
• Additional dependencies: none
• Coq namespace: MMaps
• Related publication(s):
  • Efficient Verified Red-Black Trees
  • Functors for Proofs and Programs doi:10.1007/978-3-540-24725-8_26

Building and installation instructions

The easiest way to install the latest released version of Modular Finite Maps over Ordered Types is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mmaps

To instead build and install manually, do:

git clone https://github.com/coq-community/coq-mmaps.git
cd coq-mmaps
make   # or make -j <number-of-cores-on-your-machine> 
make install

Documentation

This library of finite maps is a modernization of FMaps in Coq's standard library. Compared to FMaps, MMaps has a richer interface and provides additional finite map implementations, including a performant implementation based on red-black trees.

As starting points for understanding how to use the library, we recommend looking at MMaps.Interface and MMaps.demo.