Popular repositories Loading

1. LibHyps LibHyps Public

   A Coq library providing tactics to deal with hypothesis

   Rocq Prover 23 3

2. ill_narratives ill_narratives Public

   A development of a subset of intuitionistic linear logic, suitable for representing narratives.

   Coq 3 2

3. chord_finder chord_finder Public

   A small tool to find chords from lists of music notes, written in A B C or in "Figured bass" notations

   OCaml 1

4. landmark landmark Public

   Emacs package provinding fast navigation between buffers/positions.

   Emacs Lisp 1

5. CompCert CompCert Public

   Forked from AbsInt/CompCert

   The CompCert C verified compiler

   Coq

6. 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