Popular repositories Loading

1. abstract-machines abstract-machines Public

   Implementations in OCaml of various abstract machines

   OCaml 9

2. cic-model cic-model Public

   Set-theoretical models of various type theories (up to an extensional version of the Calculus of Inductive Constructions), aiming at proving logical consistency and strong normalization

   Coq 7 2

3. coq coq Public

   Forked from rocq-prover/rocq

   Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…

   OCaml 3 2

4. HoTT HoTT Public

   Forked from HoTT/Coq-HoTT

   Homotopy type theory

   Coq

5. Foundations Foundations Public

   Forked from UniMath/Foundations

   Development of the univalent foundations of mathematics in Coq

   Verilog

6. ocaml-bindlib ocaml-bindlib Public

   Forked from rlepigre/ocaml-bindlib

   Efficient binder representation in OCaml

   OCaml