FreeSpec is a framework for implementing, certifying, and executing impure computations in Coq.
This repository contains three Coq packages:
coq-freespec-coreprovides the foundation of the FreeSpec formalism.
coq-freespec-execprovides the means to execute impure computations implemented with the help of
coq-freespec-ffiprovides the means to use FreeSpec with
The codebase is organized as follows:
- The Coq definitions of the three theories live in the
- The OCaml source of the Coq plugins live in the
- There are examples for the three plugins in the
dune build dune install
Besides, we provide two helper scripts:
run-tests.shexecutes each Coq file living in
tests/and reports any error
build-docs.shbuilds the OCaml and Coq source documentation
Said documentations are published here.
In addition, FreeSpec has been the subject of two academic publications.
- FreeSpec: Specifying, Certifying and Executing Impure Computations in Coq (CPP'20)
- Modular Verification of Programs with Effects and Effect Handlers in Coq (FM'18)
FreeSpec is a Free Software, distributed under the terms of the MPLv2. It was initially developed within the the French Cybersecurity Agency (ANSSI).