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