He worked on the Knuth–Bendix (KB) equational proof system in 1978–1984 with Jean-Marie Hullot.
He led the Formel project in the 1980s, which developed the Caml programming language.
He organised the Colloquium “Proving and Improving Programs’’ in Arc-et-Senans in 1975, the 5th International Conference on Automated Deduction (CADE) in Les Arcs in 1980, the Logic in Computer Science Symposium (LICS) in Paris in 1994, and the First International Symposium in Sanskrit Computational Linguistics in 2007.
He was coordinator of the ESPRIT European projects Logical Frameworks, then TYPES, from 1990 to 1995.
He has made major contributions to the theory of unification and to the development of typed functional programming languages, in particular Caml.