meta.yml

---
fullname: Modular Finite Maps over Ordered Types
shortname: coq-mmaps
organization: coq-community
opam_name: coq-mmaps
community: true
action: true

synopsis: Several implementations of finite maps over arbitrary ordered types using Coq functors

description: |-
  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.

publications:
- pub_url: https://www.cs.princeton.edu/~appel/papers/redblack.pdf
  pub_title: Efficient Verified Red-Black Trees
- pub_url: https://hal.inria.fr/hal-00150913
  pub_title: Functors for Proofs and Programs
  pub_doi: 10.1007/978-3-540-24725-8_26

authors:
- name: Pierre Letouzey
  initial: true
- name: Andrew W. Appel  

maintainers:
- name: Pierre Letouzey
  nickname: letouzey
- name: Karl Palmskog
  nickname: palmskog

opam-file-maintainer: palmskog@gmail.com

opam-file-version: dev

license:
  fullname: GNU Lesser General Public License v2.1 only
  identifier: LGPL-2.1-only

supported_coq_versions:
  text: 8.14 and later
  opam: '{>= "8.14"}'

tested_coq_opam_versions:
- version: 'dev'
- version: '8.20'
- version: '8.19'
- version: '8.18'
- version: '8.17'
- version: '8.16'
- version: '8.15'
- version: '8.14'

namespace: MMaps

keywords:
- name: finite maps
- name: red-black trees
- name: AVL trees
- name: ordered types

categories:
- name: Computer Science/Data Types and Data Structures

documentation: |-
  ## Documentation

  This library of finite maps is a modernization of
  [FMaps](https://coq.inria.fr/stdlib/Coq.FSets.FMaps.html) 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](theories/RBT.v).

  As starting points for understanding how to use the library,
  we recommend looking at [MMaps.Interface](theories/Interface.v) and
  [MMaps.demo](theories/demo.v).
---