Tac/μLJ: focused inductive theorem proving

Tac is a framework for implementing interactive theorem provers with good support for both interactive proof development and automated proof search. In that framework, we implemented a focusing proof system for μLJ, i.e., intuitionistic logic with least and greatest fixed points. We showed that a relatively naive proof search procedure, built on the refined foundations provided by focusing, yields surprisingly good results. This tool also implements the lifting approach to generic quantification (cf. research paper). Learn more on the Slimmer page of tac.

Bedwyr: a proof-search approach to model-checking

Bedwyr is a logic programming language which relies on the proof-theoretic notion of fixed point definition to support an operational reading of the implication as an exhaustive case analysis. It supports λ-tree syntax (a variant of HOAS), higher-order pattern unification and generic quantification (∇). It also uses tabling to handle (co)inductive specifications in a meaningful way. Examples of use include the verification of bisimulation for the π-calculus, exploration of winning strategies for games, properties of graphs/automata... in a purely declarative way. It is available through the INRIA gforge page of the Slimmer project. (See also in my publications, the one on Bedwyr.)


Savonet is a group of developers working since 2003 on audio streaming, and netradios in particular. Our stream generator, liquidsoap, is outstandingly rich and flexible, thanks to its internal architecture (in OCaml) and its user interface through a dedicated script language. The Savonet project also brought many bindings to the OCaml community: vorbis, mad, shout, etc. Check the official homepage of savonet. (See also in my publications for more reading on Liquidsoap.)

Tiny Tools


My OCaml mode for VIm now deserves its very own page.

Rotate the pictures from your digital camera

Digital cameras store the orientation of the pictures, but do not rotate the pictures. So I wrote flipper which performs the rotation of the freshly downloaded pictures. (June 2004)

Photo gallery

I also created another photo gallery system. It is not the simplest one but I find it pretty and it allows easy modification of the site (only in French).

Frontend for jumpnbump

A frontend for the wonderful game jumpnbump : jnbsync. It allow clients not to own the level file which has been chosen by the server. It also avoids to wait infinitely for a last client, who has finally decided not to come. It's useful, and light. (October 2003)


Braidtex produces nice EPS graphics representing your braids. You can describe the braid using a very precise representation or the signature. (Summer 2003)


Ddtun is a tiny script which updates your dyndns IP. (April 2003)


Watching is a xchat plugin which beeps well. (March 2003)

School projects


My second OCaml programming project for school was to write a Lisp interpreter. We named it CUL, for Caml Ultimate Lisp. It features curryfication, tail-recursivity, lazy evaluation, static (scheme, clisp) and dynamic (emacs lisp) binding. We took great care of the code architecture. The project is waiting for you on Sourceforge. (January 2003 - updated for OCaml-3.08)


My first OCaml project was about fractal compression. It is also available on Sourceforge. (November 2002)


I worked on grapheme-phoneme transcription for the competitive exams I had during summer 2002. Everything is in french, except the C++ sources. I used statistical methods and neural networks.