A Series on coqffi

coqffi generates Coq FFI modules from compiled OCaml interface modules (.cmi). In practice, it greatly reduces the hassle to mix OCaml and Coq modules within the same codebase, especially when used together with the dune build system.

coqffi in a Nutshell

For each entry of a cmi file, coqffi tries to generate an equivalent (from the extraction mechanism perspective) Coq definition. In this article, we walk through how coqffi works.

Implementing an Echo Server in Coq with coqffi

In this tutorial, we will demonstrate how coqffi can be used to implement an echo server, i.e., a TCP server which sends back any input it receives from its clients.