Gérard Huet
Encyclopedia
Gérard Pierre Huet is a French
computer scientist.
, and the Université de Paris.
His specialities are software architecture
, design of programming language
s and of proof assistants, project management
, and international relations
.
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 was 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 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 project in the 1990s with Christine Paulin, who developed the Coq proof assistant. He invented the Zipper data structure in 1996. 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 in 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
and he is webmaster of the Sanskrit Heritage Site. In particular, he is working on Eilenberg machines
and on the formal structure of Sanskrit
.
France
The French Republic , The French Republic , The French Republic , (commonly known as France , is a unitary semi-presidential republic in Western Europe with several overseas territories and islands located on other continents and in the Indian, Pacific, and Atlantic oceans. Metropolitan France...
computer scientist.
Biography
Gérard Huet graduated from the Université Denis Diderot (Paris VII), Case Western Reserve UniversityCase Western Reserve University
Case Western Reserve University is a private research university located in Cleveland, Ohio, USA...
, and the Université de Paris.
His specialities are software architecture
Software architecture
The software architecture of a system is the set of structures needed to reason about the system, which comprise software elements, relations among them, and properties of both...
, design of programming language
Programming language
A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....
s and of proof assistants, project management
Project management
Project management is the discipline of planning, organizing, securing, and managing resources to achieve specific goals. A project is a temporary endeavor with a defined beginning and end , undertaken to meet unique goals and objectives, typically to bring about beneficial change or added value...
, and international relations
International relations
International relations is the study of relationships between countries, including the roles of states, inter-governmental organizations , international nongovernmental organizations , non-governmental organizations and multinational corporations...
.
He is senior research director at INRIA, a member of the French Academy of Sciences
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 research...
, and a member of Academia Europaea
Academia Europaea
Academia Europæa is a European non-governmental scientific academy founded in 1988. Its members are scientists and scholars who collectively aim to promote learning, education and research. It publishes European Review through Cambridge Journals....
. Formerly he was a Visiting Professor at Asian Institute of Technology
Asian Institute of Technology
The Asian Institute of Technology is an international institution for higher education in engineering, advanced technologies, and management and planning...
in Bangkok
Bangkok
Bangkok is the capital and largest urban area city in Thailand. It is known in Thai as Krung Thep Maha Nakhon or simply Krung Thep , meaning "city of angels." The full name of Bangkok is Krung Thep Mahanakhon Amon Rattanakosin Mahintharayutthaya Mahadilok Phop Noppharat Ratchathani Burirom...
, a Visiting Professor at Carnegie-Mellon University, and a Guest Researcher at SRI International
SRI International
SRI International , founded as Stanford Research Institute, is one of the world's largest contract research institutes. Based in Menlo Park, California, the trustees of Stanford University established it in 1946 as a center of innovation to support economic development in the region. It was later...
.
He was the author of a unification algorithm for simply typed lambda calculus
Simply typed lambda calculus
The simply typed lambda calculus , a formof 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 calculus...
, and of a complete proof method for Church
Alonzo Church
Alonzo Church was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church–Turing thesis, Frege–Church ontology, and the Church–Rosser theorem.-Life:Alonzo Church...
's theory of types (Constrained Resolution). He worked on the Mentor program editor in 1974–1977 with Gilles Kahn
Gilles Kahn
Gilles Kahn was a French computer scientist. He notably introduced Kahn process networks as a model for parallel processing....
. He worked on the KB equational proof system in 1978–1984 with Jean-Marie Hullot
Jean-Marie Hullot
Jean-Marie Hullot is 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, which later became Interface Builder for NeXTSTEP , and later still evolved into an important...
. He led the Formel project in the 1980s, which developed the Caml programming language. He designed the Calculus of Constructions
Calculus of constructions
The calculus of constructions is a formal language in which both computer programs and mathematical proofs can be expressed. This language forms the basis of theory behind the Coq proof assistant, which implements the derivative calculus of inductive constructions.-General traits:The CoC is a...
in 1984 with Thierry Coquand
Thierry Coquand
Thierry Coquand is a professor in computer science at the University of Gothenburg, Sweden. He is known for his work in constructive mathematics, especially the calculus of constructions. He received his Ph.D. under the supervision of Gérard Huet.- External links :*...
. He led the Coq project in the 1990s with Christine Paulin, who developed the Coq proof assistant. He invented the Zipper data structure in 1996. 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 in 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
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...
in 1980, the Logic in Computer Science Symposium (LICS) in Paris
Paris
Paris is the capital and largest city in France, situated on the river Seine, in northern France, at the heart of the Île-de-France region...
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
Functional programming
In computer science, functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions and avoids state and mutable data. It emphasizes the application of functions, in contrast to the imperative programming style, which emphasizes changes in state...
languages, in particular CAML
Caml
Caml is a dialect of the ML programming language family, developed at INRIA and formerly at ENS....
. More recently he has been a scholar on computational linguistics
Computational linguistics
Computational linguistics is an interdisciplinary field dealing with the statistical or rule-based modeling of natural language from a computational perspective....
in Sanskrit
Sanskrit
Sanskrit , is a historical Indo-Aryan language and the primary liturgical language of Hinduism, Jainism and Buddhism.Buddhism: besides Pali, see Buddhist Hybrid Sanskrit Today, it is listed as one of the 22 scheduled languages of India and is an official language of the state of Uttarakhand...
and he is webmaster of the Sanskrit Heritage Site. In particular, he is working on Eilenberg machines
X-machine
The X-machine is a theoretical model of computation introduced by Samuel Eilenberg in 1974.S. Eilenberg Automata, Languages and Machines, Vol...
and on the formal structure of Sanskrit
Sanskrit
Sanskrit , is a historical Indo-Aryan language and the primary liturgical language of Hinduism, Jainism and Buddhism.Buddhism: besides Pali, see Buddhist Hybrid Sanskrit Today, it is listed as one of the 22 scheduled languages of India and is an official language of the state of Uttarakhand...
.
Publications
- "A Unification Algorithm for Typed Lambda-Calculus", Gerard P. Huet, Theoretical Computer Science 1 (1975), 27-57
- "30 Years of Higher-Order Unification", Gérard Huet, TPHOL 2002, INRIA
- Le Projet prévision-réalisation des vols, SINCRO, Paris, 1970.
- Spécifications pour une base commune de données, SINCRO, Paris, 1971.
- A Mechanization of type theory, LABORIA, Rocquencourt, 1973.
- La Gestion des données dans les systèmes informatiques, École supérieure d'électricité, Malakoff, 1974.
External links
- Gérard Huet home page (428 pages, 5 April 2007)