Pinned Loading

1. Cryptographic Primitive Code Generation by Fiat

   Rocq Prover 816 166

3. A Coq library for Homotopy Type Theory

   Rocq Prover 1.4k 201

4. Some scripts to help construct small reproducing examples of bugs, implement [Proof using], etc.

   Python 46 9

5. Two attempts at formalizing Löb's Theorem, (one based on http://lesswrong.com/lw/t6/the_cartoon_guide_to_l%C3%B6bs_theorem/). Write-up at https://github.com/JasonGross/lob-paper

   Agda 26 2

6. The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…

   OCaml 5.4k 720