blob: f8d9695ce02cfe79648e5a8d77ae452b637aaaad (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
#+TITLE: A series on ~coqffi~
#+SERIES: ../coq.html
#+SERIES_PREV: AlgebraicDatatypes.html
~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.
- [[./CoqffiIntro.org][~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.
- [[./CoqffiEcho.org][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.
|