summaryrefslogtreecommitdiffstats
path: root/site/index.org
diff options
context:
space:
mode:
Diffstat (limited to 'site/index.org')
-rw-r--r--site/index.org6
1 files changed, 6 insertions, 0 deletions
diff --git a/site/index.org b/site/index.org
index 263395e..ea0d27b 100644
--- a/site/index.org
+++ b/site/index.org
@@ -52,6 +52,12 @@ machine-checked proofs.
means the definitions of ~+~ and ~*~ have to satisfy properties such as
commutativity or the existence of neutral elements.
+- [[./posts/Coqffi.org][A Series on ~coqffi~]] ::
+ ~coqffi~ generates Coq FFI modules from compiled OCaml interface
+ modules (~.cmi~). In practice, it greatly reduces the hassle to mix
+ together OCaml and Coq modules within the same codebase, especially
+ when used together with the ~build~ build system.
+
* About Haskell
Haskell is a pure, lazy, functional programming language with a very expressive