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.0.tar.gz
sha512=1d75e229cf3deaa654177464fee009807acb22f8f72cfb54bcf9d5ee16cc318f3ed089a1f4c94c520637b1845ba0e5fccac951cacbe6ca7e62cb9a2047b01c72

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 date:2020-01-25

Published: 01 Feb 2020

Dependencies (4)

  1. coq-infotheo >= "0.0.6" & < "0.0.7~"
  2. coq-mathcomp-analysis >= "0.2.0" & < "0.3~"
  3. coq-mathcomp-ssreflect >= "1.10" & < "1.11~"
  4. coq >= "8.10.2" & < "8.11~"

Dev Dependencies

None

Used by

None

Conflicts

None