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.0.0.tar.gz
md5=297a95b8ca4157760862e5812e8addd3

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 date:2016-10-04

Published: 04 Oct 2016

Dependencies (3)

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

Dev Dependencies

None

Used by

None

Conflicts

None