||This biographical article needs additional citations for verification. (September 2010)|
July 7, 1947 |
|Alma mater||Case Western Reserve University
University of Paris
|Doctoral advisor||George Ernst
|Doctoral students||Thierry Coquand
Gérard Pierre Huet (born July 7, 1947) is a French computer scientist.
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. In particular, he is working on Eilenberg machines and on the formal structure of Sanskrit. He is webmaster of the Sanskrit Heritage Site.
- 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
- Gérard P. Huet (1973). "A Mechanization of Type Theory". In Nils J. Nilsson. Proc. 3rd Int. Joint Conf. on Artificial Intelligence (IJCAI). William Kaufmann. pp. 139–146.
- Gérard P. Huet (1973). "The Undecidability of Unification in Third Order Logic". Information and Control 22: 257–267. doi:10.1016/s0019-9958(73)90301-x.
- 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
- Gérard Huet (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (Ph.D.). Universite de Paris VII.
- Gérard Huet, Bernard Lang (1978). "Proving and Applying Program Transformations Expressed with Second-Order Patterns". Acta Informatica 11: 31–55. doi:10.1007/bf00264598.
- Gérard Huet, D.S. Lankford (Mar 1978). On the Uniform Halting Problem for Term Rewriting Systems (Technical report). IRIA. p. 8. 283.
- G. Huet, J.M. Hullot (Oct 1980). "Proofs by Induction in Equational Theories with Constructors". 21st Ann. Symp. on Foundations of Computer Science. IEEE. pp. 96–107.
- G. Huet, D.C. Oppen (Jan 1980). Equations and Rewrite Rules: A Survey (Technical report). Stanford Univ., CS Dept. p. 52. STAN-CS-80-785.
- Gérard Huet (1981). "A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm". J. Comput. System Sci. 23 (1): 11–21. doi:10.1016/0022-0000(81)90002-7.
- Gérard Huet (May 1986). Formal Structures for Computation and Deduction. International Summer School on Logic of Programming and Calculi of Discrete Design.
- Gérard Huet (1988). K. Fuchi and M. Nivat, ed. Induction Principles Formalized in the Calculus of Constructions. North-Holland. pp. 205–216.
- Gérard Huet (Aug 1993). Residual Theory in λ-Calculus: A Formal Development (Technical report). INRIA. 2009.
- Huet, G.P. (1996). Ganzinger, Harald, ed. Design Proof Assistant (invited lecture). LNCS 1103. Springer-Verlag. p. 153.
- Gérard Huet, H. Laulhère (Sep 1997). "Finite-state Transducers as Regular Böhm Trees". In M. Abadi and T. Ito. Theoretical Aspects of Computer Software. LNCS 1281. Springer. pp. 604–610.
- Gérard Huet (1998). "Regular Böhm Trees". Math. Struct. in Comp. Science 8: 671–680. doi:10.1017/s0960129598002643.
- Gérard Huet (2002). "Higher Order Unification 30 years later". In V. Carreño and C. Muñoz and S. Tahar. Proceedings, 15th International Conference TPHOL. LNCS 2410. Springer. pp. 3–12.
- Gérard Huet (2003). Fairouz Kamareddine, ed. Linear Contexts and the Sharing Functor: Techniques for Symbolic Computation. Kluwer.
- Pawan Goyal, Gérard Huet (Jan 2013). "Completeness Analysis of a Sanskrit Reader". Proceedings of the Fifth International Symposium on Sanskrit Computational Linguistics, Mumbai.
- Gérard Huet, Pawan Goyal (Dec 2013). "Design of a lean interface for Sanskrit corpus annotation". Proceedings, ICON13, Hyderabad.
- Gérard Huet.[dead link]
- Sanskrit Heritage Site
- Gérard Huet at the Mathematics Genealogy Project
- Gérard Huet's home page (dead link?) — Gérard Huet's home page
- PDF (3.32 MB) (428 pages, 5 April 2007)