Gérard Huet

Gérard Pierre Huet (; born 7 July 1947) is a French computer scientist, linguist and mathematician. He is senior research director at INRIA and mostly known for his major and seminal contributions to type theory, programming language theory, and to the theory of computation.

Biography Gérard Huet graduated from the Université Denis Diderot (Paris VII), Case Western Reserve University, and the Université de Paris.

He is senior research director at INRIA, a member of the French Academy of Sciences, and a member of Academia Europaea. Formerly he was a visiting professor at Asian Institute of Technology in Bangkok, a visiting professor at Carnegie Mellon University, and a guest researcher at SRI International.

He is the author of a unification algorithm for simply typed lambda calculus, and of a complete proof method for Church's theory of types (constrained resolution). He worked on the Mentor program editor in 1974–1977 with Gilles Kahn. 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 designed the calculus of constructions in 1984 with Thierry Coquand. He led the Coq (renamed Rocq) proof assistant project in the 1990s with Christine Paulin-Mohring, who developed Coq. He named, exposited, and popularized the zipper data structure in 1997. He was Head of International Relations for INRIA in 1996–2000. He designed the Zen Computational Linguistics toolkit in 2000–2004.

He organized the Institute of Logical Foundations of Functional Programming during the Year of Programming at the University of Texas at Austin in Spring 1987. 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. More recently he has been a scholar on computational linguistics in Sanskrit. In particular, he is working on Eilenberg machines and on the formal structure of Sanskrit. He is webmaster of the Sanskrit Heritage Site.

Huet received the Herbrand Award in 1998 and received the EATCS Award in 2009.

Publications

Le Projet prévision-réalisation des vols, Société d'informatique, de conseils et de recherche opérationnelle (SINCRO), Paris, 1970. WorldCat Record Spécifications pour une base commune de données, SINCRO, Paris, 1971. WorldCat Record

La Gestion des données dans les systèmes informatiques, École supérieure d'électricité, Malakoff, 1974. WorldCat Record "A Unification Algorithm for Typed Lambda-Calculus", Gerard P. Huet, Theoretical Computer Science 1 (1975), 27-57

Postscript