A 3D graphic library

(CEA-DAM, Fortran, 1967);

An interactive alpha-beta procedure at varying depth demonstrated as a Kalah champion

(CWRU, Fortran, 1969);

PETER, an interactive theorem prover inspired from SAM

(CWRU, Stanford LISP, 1970);

UNIF, a complete enumerator for higher order unifiers in Church's type theory

(IRIA, ALGOL W, 1972);

Mentor, a Structured Programming Environment

(IRIA, joint work with the CROAP team, PASCAL, 1974-1977);

An algorithm to generate the basis of solutions to homogeneous linear diophantine equations

(IRIA, PASCAL, 1977).

KB, a Knuth-Bendix completion procedure including packages for AC and proof by consistency

(IRIA and SRI, joint work with Jean-Marie Hullot, VLISP, 1978-1980);

A simulator for NMOS circuits, inspired from Bryant

(IRIA, joint work with Jean-Marie Hullot, Le_LISP-CEYX, 1981);

A Complete Driver for a Mergenthaler-Lynotype photocomposer as Backend of the Multics Compose text formatter

(IRIA, joint work with Guy Cousineau, PL/1 and assembler, 1982); A hardware and P-ROM asynchronous communication driver for Multics was designed jointly with Patrick Amar but persistently failed certification.

An ML Environment adapted from Edinburgh-LCF, with compiler

(IRIA, Portable LISP, 1983); adapted to Cambridge LCF by Larry Paulson, and with concrete types by Guy Cousineau;

CAML, an ML environment for fast prototyping

(joint work with the Formel team, INRIA, CAML+LLM3, 1984-1985);

A G-machine implementation of lambda-calculus, and its application as back-end evaluator for system-F lambda-expressions

(INRIA, Le_Lisp, 1985);

The Constructive Engine, an abstract machine for the Calculus of Constructions

(INRIA, CAML, 1985);

Proofs and Computations, an executable course

(CMU, CAML, 1986);

The COC Proof Engine

(joint work with Thierry Coquand and Christine Paulin, INRIA, CAML, 1986-1991);

A GHC interpreter

(ICOT, CAML, 1987);

Constructive Computability

An executable course on lambda-calculus, including a Böhm discriminator (INRIA, Paris 7, Greco de Programmation and AIT Bangkok, CAML, 1985-91; Bordeaux, OCaml, 2003);

The Coq Proof Assistant

(team work with the Coq project, INRIA, Caml, Camllight and O'Caml, 1992-1996);

Zipper

I invented the Zipper data structure in 1995 and presented it at the Federated Logic Conference (FLoC) in 1996. No offence meant to ladies.

Zen

Nowadays my favorite occupation is programming various tasks in Ocaml. I am currently developing a computational linguistics toolkit Zen, developed in the framework of a computational linguistics platform for Sanskrit.