Welcome to the coqffi
project website! This project is part of coq-community.
coqffi
generates the necessary Coq boilerplate to use OCaml functions in a Coq development, and configures the Coq extraction mechanism accordingly.
This is an open source project, licensed under the MIT License.
The current stable release of coqffi
can be downloaded from GitHub.
The coqffi
binary comes with a comprehensive man page.
In addition, documentations for the CoqFFI
theory
are provided for the following versions: