Popular repositories Loading

1. ite-normalisation ite-normalisation Public

   L. Paulson's If-Then-Else normalisation algorithm in Coq via simulated Induction-Recursion

   Coq 9

2. Coq-Phase-Semantics Coq-Phase-Semantics Public

   Coq Source for Relational Phase Semantics and Cut-elimination

   Coq 6

3. Introduction-to-Coq Introduction-to-Coq Public

   Introduction to the Coq proof assistant

   Coq 6

4. The-Braga-Method The-Braga-Method Public

   The Braga Method for Extracting Certified OCaml from Coq code

   Coq 5 1

5. Coq-is-total Coq-is-total Public

   A proof that Coq contains any total mu-recursive function

   Coq 4

6. PC19 PC19 Public

   Exercices and Examples for the PC'19 Autumn school

   Coq 4