Ceramist Versions Save

Verified hash-based AMQ structures in Coq

1.0.1-artefact-v2

4 years ago

This release snapshots the stable functionality of the ceramist library:

  • Implementation of bloom filters
  • Implementation of counting bloom filters
  • Implementation of quotient filters
  • Implementation of higher-order AMQ - Blocked AMQ, and instantiations for the AMQs mentioned above.

Details of the implementation can be found on the associated CAV2020 paper.

1.0.1-artefact-old

4 years ago

Ceramist v1.0.1 Artefact Release

This release snapshots the stable functionality of the ceramist library:

  • Implementation of bloom filters
  • Implementation of counting bloom filters
  • Implementation of quotient filters
  • Implementation of higher-order AMQ - Blocked AMQ, and instantiations for the AMQs mentioned above.

Details of the implementation can be found on the associated CAV2020 paper.

1.0.1

4 years ago

Changelog

  • Updated to support Coq.8.11.0

1.0.0

4 years ago

Ceramist first official release

Changes

  • Rebranded to Ceramist
  • Added proof of Counting Bloom filters
  • Added proof of Quotient filters
  • Added proof of Blocked AMQs
  • Introduced interface based AMQ framework

0.0.1

4 years ago

First release of the ProbHash library.