Pinned

1. sifive/RiscvSpecFormal sifive/RiscvSpecFormal Public

   The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor mo…

   Haskell 74 8

2. functional-algebra functional-algebra Public

   This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides bot…

   Coq 28 2

3. FPU-Verification FPU-Verification Public

   Verifies that Floating Point Unit used within SiFive's S-series is correct. Specifically, that Hauser's design allocates enough bits to its rem register to prevent an overflow during floating point…

   Coq

4. pigeons pigeons Public

   A proof of the Pigeonhole principle. The Pigeonhole principle is a fundamental theorem that is used widely in Computer Science and Combinatorics, it asserts that if you put n things into m containe…

   Makefile 2

5. cluster cluster Public

   This package defines a collection of functions for clustering phrases such as names and titles into equivalence/similarity classes.

   OCaml

6. ppx_record_stats ppx_record_stats Public

   An OCaml PPX library that makes it easy to compute descriptive statistics for datasets.

   OCaml