Software
achievements of Gérard Huet

(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, 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);
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.

(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.

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);

(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.

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.

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