Pinned Loading

1. flower-prover flower-prover Public

   Can 🌸 be turned into a direct manipulation GUI for theorem proving?

   HTML 3

2. flowers-metatheory flowers-metatheory Public

   Can ✿ capture intuitionistic logic?

   Coq 1

3. flower-auto flower-auto Public

   Can ❀ decide intuitionistic propositional logic?

   OCaml 1

4. CoqHopf CoqHopf Public

   Construction of the Hopf fibration in Homotopy Type Theory, using the HoTT library for Coq.

   HTML 1

5. cbpv cbpv Public

   A study of a simplified Call-By-Push-Value lambda-calculus in Coq.

   Coq 1

6. gym-numgrid gym-numgrid Public

   An OpenAI Gym environment where an agent explores a grid of hand-written digits images.

   Python