Explore projects
-
BERTOT Yves / stdpp
BSD 3-Clause "New" or "Revised" LicenseUpdated -
Updated
-
This repository contains the Coq/Iris proofs that accompany the paper Spy game---Verifying a local generic solver in Iris
Updated -
Updated
-
pred-tv / SMTCoq
CeCILL-C Free Software License AgreementFork of https://github.com/smtcoq/smtcoq.
Topics: CoqUpdated -
Updated
-
BERTOT Yves / ProgrammezCoq
Creative Commons Attribution 4.0 InternationalUne description de la programmation en Coq pour un magazine grand public.
Updated -
Updated
-
Updated -
Apps to compile from skel to gallina for use with the Coq Proof Assistant
Updated -
Resources for course MPRI 2-4 on functional programming and type systems.
Updated -
Verifisc / Mlang
GNU General Public License v3.0 or laterDEPRECATED, MOVED TO GITHUB https://github.com/MLanguage/mlang
Updated -
DAGAND Pierre-Evariste / Mlang
GNU General Public License v3.0 or laterCompiler for the M language of the French DGFiP
Updated -
BOUR Frederic / menhir
GNU Library General Public License v2 onlyAn LR(1) parser generator for OCaml.
Updated -
Pierre-Marie Pédrot / menhir
GNU Library General Public License v2 onlyAn LR(1) parser generator for OCaml.
Updated -
Frédéric Blanqui / menhir
GNU Library General Public License v2 onlyAn LR(1) parser generator for OCaml.
Updated