name: containers-verified
version: 0.5.11.0
synopsis: Formally verified drop-in replacement of containers
description:
In the context of the <https://deepspec.org/main DeepSpec project>, parts of the
<http://hackage.haskell.org/package/containers containers> library were
formally verified using <https://github.com/antalsz/hs-to-coq hs-to-coq> and
the interactive theorem prover Coq.
.
This package depends on precisely the verified version of containers and
re-exports the verified parts of the API, with module name and function name
unchanged.
.
If you happen to use only the verified subset of the API, then you can simply change
@containers@ to @containers-verified@ in your @.cabal@ file and earn bragging
rights about using verified data structures in your project. Because the
types from @containers@ are re-exported, you can still interface with other
libraries that depend on @containers@ directly.
.
If you happen to need additional modules or functions, you will have to
depend on both @containers@ and @containers-verified@, and use
<https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#package-qualified-imports package-qualified imports> to disambiguate.
.
This package does not re-export any of the @….Internals@ modules.
.
We cannot control which type class instances are re-exported; these therefore
may give you access to unverified code. Also, the @conatiners@ code contains
some CPP directives; these can enable different code on your machine than the
code that we verified (e.g. different bit-widths).
.
To learn more about what exactly has been verified, and how wide the
formalization gap is, see the paper “Ready, Set, Verify! Applying hs-to-coq
to non-trivial Haskell code” by Joachim Breitner, Antal Spector-Zabusky, Yao
Li, Christine Rizkallah, John Wiegley and Stephanie Weirich.
.
The long-term maintenance plan for this package is not fleshed out yet, and
certainly depends on user-demand. Let us know your needs! (And your
technical or financial abilities to contribute...)
homepage: https://github.com/nomeata/containers-verified
license: MIT
license-file: LICENSE
author: Joachim Breitner
maintainer: mail@joachim-breitner.de
copyright: 2018 Joachim Breitner
category: Data
build-type: Simple
extra-source-files: ChangeLog.md
cabal-version: >=1.10
library
build-depends: containers ==0.5.11.0
default-language: Haskell2010
exposed-modules:
Data.Set
Data.IntSet
Data.Map
source-repository head
type: git
location: http://github.com/nomeata/containers-verified