Jean-Christophe Filliâtre : Programming

OCaml software

During my idle time, I develop software, mainly in OCaml, a functional programming language with a wonderful standard library and a compiler (bytecode and native) which can rival with gcc. OCaml code being fully portable, you can compile the following code on any platform supported by OCaml: Linux, most commercial UNIX, but also MacOS, Windows, etc. (unless a specificity of some platform is used, like the SVGA library for instance).

Unless stated otherwise, the code available on this page is distributed under the terms of the GNU Library General Public License version 2, with the special exception on linking described in file LICENSE.

About the links above:

The .ps are PostScript files automatically generated from the OCaml source code using ocamlweb.
The .ml and .mli have been produced with Sébastien Ailleret's (now Martin Jambon's) caml2html.
Click on the library / application name to download.
When a github repository or an opam package exists, a link is given.

Data Structures

Vector : Dynamic/growable/resizable arrays (.mli / .ml)
Parray : Persistent arrays (.mli / .ml) ; see this article
Puf : Persistent Union-Find (.mli / .ml) ; see this article
Creal : exact real arithmetic
Bitv : a bit vectors library (github | opam)
Bitset : bit vectors for small sets of integers (.mli | .ml) ;
Arbres de PatriciaPatricia trees : Efficient sets and maps over integers (ptset | ptmap) from a paper by Chris Okasaki
See also the related module Hashcons, Hset and Hmap below (to use Patricia trees on hash-consed values)
Trie : Maps over lists (.mli | .ml)
Heaps : (aka priority queues)
- traditional imperative implementation using an array (.mli | .ml)
- Braun trees (.mli | .ml)
- Leftist heaps (.mli | .ml)
Rbset : red-black trees (.ps | .mli)
This code has been certified using Coq; see this page
Hashset : Sets coded as hash tables (easier to use and slightly more compact than using the Hashtbl module) (.ps | .mli)
Suffix_tree : Ukkonen's algorithm (.mli | .ml)
Ropes : the rope data structure (.mli | .ml)
A quick, dirty and incomplete text editor using ropes: editor.ml (requires ocamlsdl, see below)
Rbuffer : (.mli | .ml) Ropes-based implementation of module Buffer; for general-purpose ropes, see above.
Poly : Polynomials with coefficients in any ring (.mli | .ml)
Bdd : Binary decision diagrams (BDDs) (.mli)

Libraries

Combine, a library for combinatorics (with Remy El Sibaïe) (github | opam)
Functory, a library for distributed computing, inspired by MapReduce (with Kalyan Krishnamani) (github)
OCamlgraph, an OCaml graph library (github | opam)
Mlpost, an OCaml drawing library (github | opam)
cgi : a short library to write CGIs (.mli)
ocamlsvga : interface for the Linux SVGAlib library
ocamlsdl : interface for the SDL games library; includes support functions for OpenGL, to be used for instance with the lablGL bindings

Note: there exists a similar, more advanced, project at OcamlSDL.sourceforge.net
display : visualization of the internal representation of Caml values (.ps | .mli)
hashcons : hash tables for hash consing (.ps | .mli | github). This technique is described in this paper.
Hset / Hmap: Specialized Ptset and Ptmap modules (see above) on hash-consed values (hset.mli | hmap.mli).
prtree : to print trees in a pstree-like way (.ps | .mli)
search : functorized code for depth-first, breadth-first and iterative deepening searches (.ps | .mli)

Applications

bibtex2html : BibTeX to HTML converter
ocamlweb : a literate programming tool for OCaml (opam)
ocamlwc : a program to count the lines of code and documentation in OCaml sources (.ps)
yamlpp : a very simple HTML preprocessor, inspired by Nicolas Thiery's htmlpp

Algorithmic

Garsia-Wachs algorithm : implementation following The Art of Computer Prorgamming ; detailed description of this OCaml code in this article (.mli / .ml)
Delaunay triangulation : implements D. Knuth's algorithm from Axioms and Hulls. Complexity: O(N log N) time on the average; always O(N) space. Applies to any CCC system (see Axioms and Hulls). Note: this module is part of OCamlgraph but may be used independently. (.mli)
DLX: Implementation of D. Knuth's Dancing Links algorithm (.mli / .ml / .ps)
See also the library Combine.
Knuth-Morris-Pratt string searching algorithm (.mli / .ml / .ps)
Pentaminos : Computation of the number of solutions
Solitaire : search of the solution (french solitaire) (.ps), with the help of Xavier Urbain. (in French)
anagram.ml : Anagrams (.ps). To test it, here is a dictionary
koda-ruskey.ml : Implementation of the Koda-Ruskey algorithm (.ps), inspired by D. E. Knuth implementation
This code is detailed in this article (co-authored with François Pottier)