A 3D graphic library with stereoscopic vision and animation

(CEA-DAM, Fortran 4, 1967); this effort is documented here.

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

(CWRU, Fortran, 1969);

PETER, an interactive first-order theorem prover with equality inspired from SAM

(CWRU, Stanford LISP, 1970);

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

(IRIA, ALGOL W, 1974); The source code of this program is available as a pdf document. Calling conventions and an exemple of execution are given in a README.

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;

Formel, an adaptation of LCF to do equational reasoning with KB.

This merge of LCF and KB within a Le_Lisp backend, was a proof of concept software developed for demonstration at the first meeting of the GRECO de Programmation at University of Bordeaux in March 1982. An mp4 video of this demonstration is available here.

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); this is documented in the following pdf article.

Proofs and Computations, an executable course

(CMU, CAML, 1986); The course notes are available as the following pdf document Formal Structures for Computation and Deduction.

CONSTR, an interactive prover for the Calculus of Constructions

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

A GHC interpreter

(ICOT, CAML, 1988); this effort is documented in the following pdf unpublished report.

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 OCaml, 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

a computational linguistics toolkit (joint work with Benoît Razet, Inria, Ocaml, 2002-2008)

Eilenberg machines

With Benoît Razet I worked out a general paradigm for Relational Programming, based on Eilenberg machines.

The Sanskrit Heritage Platform

A set of Web services for Sanskrit Computational Linguistics (Inria, Ocaml, 2000-ongoing).