Menhir

gallium.inria.frsite

Parser generator that can output Coq code for verified parsers.

from

OCaml, Coq

added

2026-10-10

likes

0

similar

1. ▲
   CFML gitlab.inria.fr

   site category #coq link ↗

   Tool for proving properties of OCaml programs in separation logic.

   
2. ▲
   CoqOfOCaml github.com

   tool category #coq link ↗

   Tool for generating idiomatic Coq from OCaml code.

   
3. ▲
   SerAPI github.com

   tool category #coq link ↗

   Tools and OCaml library for (de)serialization of Coq code to and from JSON and S-expressions.

   
4. ▲
   ocaml-parsing github.com

   tool category #ocaml link ↗
   
5. ▲
   Coq coq.inria.fr

   site category #ocaml link ↗
   
6. ▲
   jsonm erratique.ch

   site category #ocaml link ↗

OCaml › Compilers and Compiler Tools: “Menhir is a LR(1) parser generator for OCaml.”

Coq › Projects > Tools: “Parser generator that can output Coq code for verified parsers.”