CFML

gitlab.inria.frsite

Tool for proving properties of OCaml programs in separation logic.

from

Coq

added

2026-10-10

likes

0

similar

1. ▲
   Program Logics for Certified Compilers cs.princeton.edu

   site category #coq link ↗

   Book that explains how to construct program logics using separation logic, accompanied by a formal model in Coq which is applied to the Clight programming language and other examples.

2. ▲
   FCF github.com

   tool category #coq link ↗

   Framework for proofs of cryptography.

   
3. ▲
   Program Logics github.com

   tool category #coq link ↗

   Companion Coq sources for a course on program logics at Collège de France.

   
4. ▲
   Volume 6: Separation Logic Foundations softwarefoundations.cis.upenn.edu

   site category #coq link ↗

   An introduction to separation logic and how to build program verification tools on top of it.

5. ▲
   Menhir gallium.inria.fr

   site category #ocaml link ↗

   Parser generator that can output Coq code for verified parsers.

6. ▲
   Foundations of Separation Logic chargueraud.org

   site category #coq link ↗

   Introduction to using separation logic to reason about sequential imperative programs in Coq.

Coq › Projects > Tools: “Tool for proving properties of OCaml programs in separation logic.”