Pinned Loading

1. formal-land/rocq-of-ocaml formal-land/rocq-of-ocaml Public

   Formal verification for OCaml, with Rocq

   OCaml 278 22

2. HOL-Theorem-Prover/HOL HOL-Theorem-Prover/HOL Public

   Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.

   Standard ML 764 177

3. coquedille coquedille Public

   A Coq to Cedille compiler written in Coq

   Rocq Prover 34 2

4. sifive/Kami sifive/Kami Public

   Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older versio…

   Coq 232 13

5. JVM JVM Public

   An implementation of the Java Virtual Machine v1.8

   HTML 3

6. design-patterns-for-humans/brazilian-portuguese design-patterns-for-humans/brazilian-portuguese Public

   Brazilian portuguese translation [WIP]

   251 37