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 ''Institut de recherche en informatiq ...

and mostly known for his major and seminal contributions to

type theory In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a fou ...

, programming language theory 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 algorithmic efficiency, efficiently they can be solved or t ...

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

, a member of the French Academy of Sciences, 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 Europea ...

. Formerly he was a visiting professor at Asian Institute of Technology in

Bangkok Bangkok, officially known in 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 estimated populati ...

, a visiting professor at Carnegie Mellon University, and a guest researcher at

SRI International SRI International (SRI) is an American nonprofit scientific research institute and organization headquartered in Menlo Park, California. The trustees of Stanford University established SRI in 1946 as a center of innovation to support economic ...

. He is the author of a unification algorithm for

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

, and of a complete proof method for

Church Church may refer to: Religion * Church (building), a building for Christian religious activities * Church (congregation), a local congregation of a Christian denomination * Church service, a formalized period of Christian communal worship * C ...

's theory of types ( constrained resolution). He worked on the Mentor program editor in 1974–1977 with

Gilles Kahn Gilles Kahn (April 17, 1946 – February 9, 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 l ...

. 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 the SOS Interface for the Mac, whi ...

. 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 programming language which is a dialect of the ML programming language family. Caml was developed in France at INRIA and ENS. Caml is ...

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 reason, ...

in 1984 with Thierry Coquand. He led the Coq project in the 1990s with Christine Paulin-Mohring, who developed the Coq proof assistant. He invented the zipper data structure in 1996. 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 research university in Austin, Texas. It was founded in 1883 and is the oldest institution in the University of Texas System. With 40,916 undergraduate students, 11,07 ...

in Spring 1987. He organised the Colloquium “Proving and Improving Programs’’ in

Arc-et-Senans Arc-et-Senans () is a commune in the Doubs department in the Bourgogne-Franche-Comté region of eastern France. The Royal Saltworks, a UNESCO World Heritage Site since 1982, is located here. Geography Arc-et-Senans is a large commune located ...

in 1975, the 5th International

Conference on Automated Deduction The Conference on Automated Deduction (CADE) is the premier academic conference on automated deduction and related fields. The first CADE was organized in 1974 at the Argonne National Laboratory near Chicago. Most CADE meetings have been held in Eu ...

(CADE) in Les Arcs 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, most populous city of France, with an estimated population of 2,165,423 residents in 2019 in an area of more than 105 km² (41 sq mi), ma ...

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 In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that ...

languages, in particular

. More recently he has been a scholar on computational linguistics in

Sanskrit Sanskrit (; attributively , ; nominally , , ) is a classical language belonging to the Indo-Aryan branch of the Indo-European languages. It arose in South Asia after its predecessor languages had diffused there from the northwest in the late ...

. 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 in 1998 and received the EATCS Award 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's home page
* 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 Members of the French Academy of Sciences Members of Academia Europaea Formal methods people Chevaliers of the Légion d'honneur