package coq-ceramist

  1. Overview
  2. No Docs
Coq library for reasoning about probabilistic algorithms

Install

Dune Dependency

github.com Edit opam file Versions (2)

Authors

  1. K
    Kiran Gopinathan
  2. I
    Ilya Sergey

Maintainers

  1. K
    kirang@comp.nus.edu.sg

Sources

1.0.1.tar.gz
sha512=0b5a9a7fa1a68bbe90806a9cf0f603dd8f00ad9e37c86e1c8cf70d05886d11e754937838ab0f335c04c0eb0b622c49f1f6c46509880d3f9c47769d9c159defaa

Description

Ceramist extends coq-infotheo to support reasoning about probabilistic algorithms, and includes a collection of lemmas on random oracle based hash functions.

Provides an example implementation of a bloom filter and uses the library to prove the probability of a false positive.

Tags

category:Computer Science/Data Types and Data Structures keyword: bloomfilter keyword: probability keyword: amq date:2020-04-06

Published: 06 Apr 2020

Dependencies (4)

  1. coq-infotheo >= "0.1" & < "0.2~"
  2. coq-mathcomp-analysis >= "0.2.3" & < "0.3~"
  3. coq-mathcomp-ssreflect >= "1.10" & < "1.11~"
  4. coq >= "8.11.0"

Dev Dependencies

None

Used by

None

Conflicts

None