Gérard Huet

Membre de l'Institut de France (Académie des Sciences).
Member Academia Europaea.
Directeur de Recherche Émérite Inria.
Chercheur au Centre Inria de Paris.
Responsable français de l'Équipe associée Sanskrit avec l'Université d'Hyderabad.
Membre du Comité National Français d'Histoire et de Philosophie des Sciences.
Member, Board of Directors, Sanskrit Library.
Webmaster Sanskrit Heritage site.
Convenor First International Symposium on Sanskrit Computational Linguistics.

Research Interests

LOGIC:

Type Theory; Sequent Calculus; Linear logic; Proof nets; Constructive Mathematics; Automation of Reasoning; Proof Assistants.

COMPUTATION THEORY:

Semantics of programming languages; Lambda-calculus; Unification; Induction; Categorical models; Sequentiality; Interaction combinators.

ALGORITHMICS:

Finite-state machines; Regular relations; Transducers; Formal computing; Relational machines.

FORMAL METHODS:

Specification Languages; Type theoretical frameworks; Program validation; Certification of Safety-Critical Software; Certified Mobile Code.

PROGRAMMING LANGUAGES:

Functional Programming; ML; Logic and Constraints Programming; Relational Programming.

SOFTWARE ENGINEERING:

Literate Programming; Programming Environments; Software Architecture; Extreme Programming.

LINGUISTICS ENGINEERING:

Computational Linguistics; Lexicon; Morphology; Segmentation; Dependency grammars; Semantics; Pivot Languages; Sanskrit.

KNOWLEDGE ENGINEERING:

Semantic nets; Description logics; Mobile truth; Web services; Digital libraries.

HUMANITIES and ARTS:

Linguistics; Semiology; Ethnology; Cultural Heritage; Indian Civilization.

SOCIAL SCIENCES:

Education; Research methodology, evaluation and prospective; International Relations; Sustainable development.

PRACTICE:

Mountaineering, trecking; Sailing; Travels; Yoga.

Academic Life

My participation in academic life worldwide is listed here.

Teaching

Documents for the 2004 course "Calculs algébriques et fonctionnels" may be found here. My executable course notes on lambda-calculus are available here as a pdf document. The executable Ocaml sources are freely downlodable from the Constructive Computation Theory site.

The Fall 2008 course notes for MPRI's "Linguistic Modelling using Logical and Computational Tools" is available here as a pdf document.

Publications

My main publications are listed here. The latest ones may be downloaded from there.

My Google scholar citations page.

Software projects

My main software projects are listed here.

Recent Talks

Recent presentations are available here.

Capsule biography

In May 68 I got my pilot license while training as an Aerospace engineer. I learnt programming in PAF on a CAB 500 computer, in Algol 60 on a CAE 510, in Fortran on an IBM 7094, and in LISP 1.5 on a PDP 10. In the 70's I investigated lambda-calculus, higher-order unification and equational logic, and I worked on the programming environment Mentor with Gilles Kahn in the legendary bâtiment 8 in the historical original IRIA site of Rocquencourt. In the 80's I headed the Formel project that developed the Caml functional programming language and the Calculus of Constructions logical framework. In the 90's I worked on Type Theory, coordinated the European Logical Frameworks then Types Basic Research Actions, and headed the Coq project-team that developed the Coq proof assistant. In 1992 I invented the Zipper data structure. From 1997 to 1999 I took a research break and assumed the position of International Relations Head at Inria Headquarters. I traveled a lot, I often wore a tie, and I was a tough negociator. In 2000 I came back to research in Computational Linguistics, and developed the Zen toolkit for finite-state computation, the Aum transducers applicative structure, and the Sanskrit Heritage linguistic platform. In 2009 I was awarded a shawl for my Sanskrit work. In 2005-2010 I worked on effective Eilenberg machines and the Relational Programming methodology with Benoît Razet. Nowadays I work mostly on Sanskrit Computational Linguistics within a joint team between Inria and University of Hyderabad, as an experiment in Numerical Humanities.

I received the Herbrand award in 1998. I was awarded an Honoris Causa Doctorate in Technology by Chalmers University in Göteborg in April 2004. I wore my best costume. In 2009 I became recipient of the EATCS Award. I wore my second best costume. In 2011 I was awarded the Inria "Grand Prix". I was awarded the ACM-Sigplan Programming Languages Software Award in 2013 and the ACM Software Award in 2014 for the Coq proof assistant.

The International Conference Formal Structures for Computation and Deduction has been named in recognition of the influence of the 1986 eponym course notes.

I was last seen in Mumbai.

A short biodata.

My academic biodata.

My academic filiation.

My mathematical genealogy.

My Linkedin profile.

Halte au dopage !

An interview by Dominique Chouchan in 2003.

Another interview about Caml in Software Engineering Daily on November 6, 2015.

I appeared in Entrevue in its June 2008 issue. Their paparazzi spotted me in Delhi.

I discussed esthetics of programming in the Binaire Blog in March 2015.