verse-lab/ceramist
View on GitHub ↗ ★ 128 Coq
Verified hash-based AMQ structures in Coq
3 mentions on Hacker News by 2 people: 0 stories, 3 comments · first 2020-07-25 · latest 2020-07-25
20082026
-
The actual Coq code is here: https://github.com/certichain/ceramist/blob/fd5e522f2c381f7d...
comment by ur-whale · 2020-07-25 · in Bloom filters debunked: Dispelling 30 Years of bad math with Coq -
…of the Bloomfilter[2], which is fairly simple and easy to check as being correct. [1] https://github.com/certichain/ceramist/blob/fd5e522f2c381f7d... [2] https://github.com/certichain/ceramist/blob/fd5e522f2c381f7d...
comment by gopiandcode · 2020-07-25 · in Bloom filters debunked: Dispelling 30 Years of bad math with Coq -
…at the sources, I think the following commit was around the place where I was working on this: https://github.com/certichain/ceramist/commit/70927c5b50e21a...
comment by gopiandcode · 2020-07-25 · in Bloom filters debunked: Dispelling 30 Years of bad math with Coq