Gérard Pierre Huet (; born 7 July 1947) is a French computer scientist, linguist and mathematician. He is senior research director at

INRIA The National Institute for Research in Digital Science and Technology (Inria) () is a French national research institution focusing on computer science and applied mathematics. It was created under the name French Institute for Research in Comp ...

and mostly known for his major and seminal contributions to

type theory In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundation of ...

programming language theory Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is clos ...

and to the

theory of computation In theoretical computer science and mathematics, the theory of computation is the branch that deals with what problems can be solved on a model of computation, using an algorithm, how efficiently they can be solved or to what degree (e.g., app ...

Biography

Gérard Huet graduated from the Université Denis Diderot (Paris VII),

Case Western Reserve University Case Western Reserve University (CWRU) is a Private university, private research university in Cleveland, Ohio, United States. It was established in 1967 by a merger between Western Reserve University and the Case Institute of Technology. Case ...

, and the

Université de Paris The University of Paris (), known metonymically as the Sorbonne (), was the leading university in Paris, France, from 1150 to 1970, except for 1793–1806 during the French Revolution. Emerging around 1150 as a corporation associated with the cat ...

. He is senior research director at

, a member of the

French Academy of Sciences The French Academy of Sciences (, ) is a learned society, founded in 1666 by Louis XIV at the suggestion of Jean-Baptiste Colbert, to encourage and protect the spirit of French Scientific method, scientific research. It was at the forefron ...

, and a member of

Academia Europaea The Academia Europaea is a pan-European Academy of humanities, letters, law, and sciences. The Academia was founded in 1988 as a functioning Europe-wide Academy that encompasses all fields of scholarly inquiry. It acts as co-ordinator of Europe ...

. Formerly he was a visiting professor at

Asian Institute of Technology The Asian Institute of Technology (AIT), founded in 1959, is an international organization for higher education situated 40 km north of Bangkok, Thailand. It specializes in engineering, advanced technologies, sustainable development, and ...

Bangkok Bangkok, officially known in Thai language, Thai as Krung Thep Maha Nakhon and colloquially as Krung Thep, is the capital and most populous city of Thailand. The city occupies in the Chao Phraya River delta in central Thailand and has an estim ...

, a visiting professor at

Carnegie Mellon University Carnegie Mellon University (CMU) is a private research university in Pittsburgh, Pennsylvania, United States. The institution was established in 1900 by Andrew Carnegie as the Carnegie Technical Schools. In 1912, it became the Carnegie Institu ...

, and a guest researcher at

SRI International SRI International (SRI) is a nonprofit organization, nonprofit scientific research, scientific research institute and organization headquartered in Menlo Park, California, United States. It was established in 1946 by trustees of Stanford Univer ...

. He is the author of a unification algorithm for

simply typed lambda calculus The simply typed lambda calculus (), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor () that builds function types. It is the canonical and simplest example of a typed lambda calculus. The ...

, and of a

complete Complete may refer to: Logic * Completeness (logic) * Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable Mathematics * The completeness of the real numbers, which implies t ...

proof method for

Church Church may refer to: Religion * Church (building), a place/building for Christian religious activities and praying * Church (congregation), a local congregation of a Christian denomination * Church service, a formalized period of Christian comm ...

's theory of types (

constrained resolution Constraint may refer to: * Constraint (computer-aided design), a demarcation of geometrical characteristics between two or more entities or solid modeling bodies * Constraint (mathematics), a condition of an optimization problem that the solution m ...

). He worked on the Mentor program editor in 1974–1977 with

Gilles Kahn Gilles Kahn (17 April 1946 – 9 February 2006) was a French computer scientist. He notably introduced Kahn process networks as a model for parallel processing and natural semantics for describing the operational semantics of programming la ...

. He worked on the Knuth–Bendix (KB) equational proof system in 1978–1984 with

Jean-Marie Hullot Jean-Marie Hullot (February 16, 1954 – June 17, 2019) was a French computer scientist and programmer who authored important programs for the original Macintosh, NeXTSTEP and Mac OS X platforms. These include SOS Interface for the Mac, which lat ...

. He led the Formel project in the 1980s, which developed the

Caml Caml (originally an acronym for Categorical Abstract Machine Language) is a multi-paradigm, general-purpose, high-level, functional programming language which is a dialect of the ML programming language family. Caml was developed in France ...

programming language. He designed the

calculus of constructions In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reaso ...

in 1984 with

Thierry Coquand Thierry Coquand (; born 18 April 1961) is a French computer scientist and mathematician who is currently a professor of computer science at the University of Gothenburg, having previously worked at INRIA. He is known for his work in constructive ...

. He led the Coq project in the 1990s with Christine Paulin-Mohring, who developed the Coq proof assistant. He named, exposited, and popularized the

zipper data structure A zipper (N. America), zip, zip fastener (UK), formerly known as a clasp locker, is a commonly used device for binding together two edges of fabric or other flexible material. Used in clothing (e.g. jackets and jeans), luggage and other bags, ...

in 1997. He was Head of International Relations for

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 The University of Texas at Austin (UT Austin, UT, or Texas) is a public university, public research university in Austin, Texas, United States. Founded in 1883, it is the flagship institution of the University of Texas System. With 53,082 stud ...

in Spring 1987. He organised the Colloquium “Proving and Improving Programs’’ in Arc-et-Senans in 1975, the 5th International

Conference on Automated Deduction A conference is a meeting, often lasting a few days, which is organized on a particular subject, or to bring together people who have a common interest. Conferences can be used as a form of group decision-making, although discussion, not always ...

(CADE) in

Les Arcs Les Arcs () is a ski resort located in Savoie, France, in the Tarentaise Valley town of Bourg-Saint-Maurice. Initially created by Robert Blanc and Roger Godino, it is a part of the huge Paradiski system which is under ownership by Compagnie ...

in 1980, the

Logic in Computer Science Logic in computer science covers the overlap between the field of logic and that of computer science. The topic can essentially be divided into three main areas: * Theoretical foundations and analysis * Use of computer technology to aid logicians ...

Symposium (LICS) in

Paris Paris () is the Capital city, capital and List of communes in France with over 20,000 inhabitants, largest city of France. With an estimated population of 2,048,472 residents in January 2025 in an area of more than , Paris is the List of ci ...

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 Unification or unification theory may refer to: Computer science * Unification (computer science), the act of identifying two terms with a suitable substitution * Unification (graph theory), the computation of the most general graph that subs ...

and to the development of typed

functional programming In computer science, functional programming is a programming paradigm where programs are constructed by Function application, applying and Function composition (computer science), composing Function (computer science), functions. It is a declarat ...

languages, in particular

. More recently he has been a scholar on

computational linguistics Computational linguistics is an interdisciplinary field concerned with the computational modelling of natural language, as well as the study of appropriate computational approaches to linguistic questions. In general, computational linguistics ...

Sanskrit Sanskrit (; stem form ; nominal singular , ,) is a classical language belonging to the Indo-Aryan languages, Indo-Aryan branch of the Indo-European languages. It arose in northwest South Asia after its predecessor languages had Trans-cultural ...

. In particular, he is working on Eilenberg machines and on the formal structure of

. He is webmaster of the Sanskrit Heritage Site. Huet received the

Herbrand Award The Herbrand Award for Distinguished Contributions to Automated Reasoning is an award given by the Conference on Automated Deduction (CADE), Inc., (although it predates the formal incorporation of CADE) to honour persons or groups for important con ...

in 1998 and received the

EATCS Award The European Association for Theoretical Computer Science (EATCS) is an international organization with a European focus, founded in 1972. Its aim is to facilitate the exchange of ideas and results among theoretical computer scientists as well as ...

in 2009.The European Association for Theoretical Computer Science Award
/ref>

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
*

References

External links

* * * Gérard Huet: :- Sanskrit Heritage Site

Retrieved 29 July 2020. :- ''Dictionnaire Héritage du Sanscrit'': pdf.downloadable version, regularly updated by the author

Retrieved 29 July 2020. :- Online ''DICO version'' (home page)

Retrieved 29 July 2020. {{DEFAULTSORT:Huet, Gerard 1947 births Living people Scientists from Bourges University of Paris alumni Case Western Reserve University alumni French computer scientists Programming language researchers Programming language designers Members of the French Academy of Sciences Members of Academia Europaea Formal methods people Knights of the Legion of Honour Academic staff of the Asian Institute of Technology