Popular repositories Loading

1. fiat-crypto fiat-crypto Public

   Forked from mit-plv/fiat-crypto

   Cryptographic Primitive Code Generation by Fiat

   Coq

2. rewriter rewriter Public

   Forked from mit-plv/rewriter

   Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting

   Coq

3. bedrock2 bedrock2 Public

   Forked from mit-plv/bedrock2

   A work-in-progress language and compiler for verified low-level programming

   Coq

4. riscv-coq riscv-coq Public

   Forked from mit-plv/riscv-coq

   RISC-V Specification in Coq

   Coq

5. equivalence equivalence Public

   Coq

6. coqutil coqutil Public

   Forked from mit-plv/coqutil

   Coq library for tactics, basic definitions, sets, maps

   Coq