package coq-msets-extra

  1. Overview
  2. No Docs
Extensions of MSets for Efficient Execution

Install

Dune Dependency

github.com Edit opam file Versions (3)

Authors

  1. F
    FireEye Formal Methods Team <formal-methods@fireeye.com>
  2. T
    Thomas Tuerk <thomas@tuerk-brechen.de>

Maintainers

  1. T
    thomas@tuerk-brechen.de

Sources

1.2.0.tar.gz
sha256=e886237194cde8602dbf191d3db7b1c28c6231c1c42996ca1b1819db3ab339ef

Description

Coq's MSet library provides various, reasonably efficient finite set implementations. Nevertheless, FireEye was struggling with performance issues. This library contains extensions to Coq's MSet library that helped the FireEye Formal Methods team (formal-methods@fireeye.com), solve these performance issues. There are

  • Fold With Abort efficient folding with possibility to start late and stop early

  • Interval Sets a memory efficient representation of sets of numbers

  • Unsorted Lists with Duplicates

Tags

keyword:finite sets keyword:fold with abort keyword:extracting efficient code keyword:data structures category:Computer Science/Data Types and Data Structures category:Miscellaneous/Extracted Programs/Data structures logpath:MSetsExtra date:2019-09-19

Published: 19 Sep 2019

Dependencies (3)

  1. coq-mathcomp-ssreflect >= "1.6"
  2. coq >= "8.9" & < "8.10~"
  3. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None