A Mechanization of Type Theory. - Gérard P. Huet (IJCAI, 1973)

The Undecidability of Unification in Third Order Logic - Gérard P. Huet (Inf. Control., 1973)

unification in typed lambda calculus. - Gérard P. Huet (Lambda-Calculus and Computer Science Theory, 1975)

A Unification Algorithm for Typed lambda-Calculus. - Gérard P. Huet (Theor. Comput. Sci., 1975)

Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems - Gérard P. Huet (FOCS, 1977)

Artificial Intelligence in Western Europe. - Jacques Pitrat; Erik Sandewall; Wolfgang Bibel; Gérard P. Huet; Hans-Hellmut Nagel; M. Somalivco (IJCAI, 1977)

Proving and Applying Program Transformations Expressed with Second-Order Patterns. - Gérard P. Huet; Bernard Lang (Acta Informatica, 1978)

An Algorithm to Generate the Basis of Solutions to Homogeneous Linear Diophantine Equations. - Gérard P. Huet (Inf. Process. Lett., 1978)

Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems. - Gérard P. Huet (J. ACM, 1980)

A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm. - Gérard P. Huet (J. Comput. Syst. Sci., 1981)

In Defense of Programming Languages Design. - Gérard P. Huet (ECAI, 1982)

Proofs by Induction in Equational Theories with Constructors. - Gérard P. Huet; Jean-Marie Hullot (J. Comput. Syst. Sci., 1982)

The future of symbolic computation: mathematics versus languages. - Gérard P. Huet (SIGSAM Bull., 1984)

Deduction and Computation. - Gérard P. Huet (Advanced Course: Fundamentals of Artificial Intelligence, 1985)

Constructions: A Higher Order Proof System for Mechanizing Mathematics. - Thierry Coquand; Gérard P. Huet (European Conference on Computer Algebra (1), 1985)

Cartesian closed Categories and Lambda- calculus. - Gérard P. Huet (Combinators and Functional Programming Languages, 1985)

Concepts mathématiques et informatiques formalisés dans le calcul des constructions. - Thierry Coquand; Gérard P. Huet (Logic Colloquium, 1985)

A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction. - Thierry Coquand; Gérard P. Huet (J. Symb. Comput., 1985)

Mechanizing Constructive Proofs (Abstract). - Gérard P. Huet (CADE, 1986)

Theorem Proving Systems of the Formel Project. - Gérard P. Huet (CADE, 1986)

Complete Sets of Unifiers and Matchers in Equational Theories. - François Fages; Gérard P. Huet (Theor. Comput. Sci., 1986)

The Calculus of Constructions: State of the Art. - Gérard P. Huet (FSTTCS, 1987)

Induction Principles Formalized in the Calculus of Constructions. - Gérard P. Huet (TAPSOFT, Vol.1, 1987)

The Calculus of Constructions - Thierry Coquand; Gérard P. Huet (Inf. Comput., 1988)

The Constructive Engine. - Gérard P. Huet (A Perspective in Theoretical Computer Science, 1989)

Design Issues for a Computer-aided Environment for Constructive Mathematics (Abstract). - Gérard P. Huet (DISCO, 1990)

Computations in Orthogonal Rewriting Systems, I. - Gérard P. Huet; Jean-Jacques Lévy (Computational Logic - Essays in Honor of Alan Robinson, 1991)

Computations in Orthogonal Rewriting Systems, II. - Gérard P. Huet; Jean-Jacques Lévy (Computational Logic - Essays in Honor of Alan Robinson, 1991)

The Gallina Specification language: A Case Study. - Gérard P. Huet (FSTTCS, 1992)

An Analysis of Böhm's Theorem. - Gérard P. Huet (Theor. Comput. Sci., 1993)

Residual Theory in lambda-Calculus: A Formal Development. - Gérard P. Huet (J. Funct. Program., 1994)

Design Proof Assistant (Abstract). - Gérard P. Huet (RTA, 1996)

Finite-State Transducers as Regular Böhm Trees. - Gérard P. Huet; Henri Laulhère (TACS, 1997)

The Zipper. - Gérard P. Huet (J. Funct. Program., 1997)

Regular Böhm trees. - Gérard P. Huet (Math. Struct. Comput. Sci., 1998)

Constructive category theory. - Gérard P. Huet; Amokrane Saïbi (Proof, Language, and Interaction, 2000)

From an Informal Textual Lexicon to a Well-Structured Lexical Database: An Experiment in Data Reverse Engineering. - Gérard P. Huet (WCRE, 2001)

Higher Order Unification 30 Years Later. - Gérard P. Huet (TPHOLs, 2002)

Srl Yantra Geometry. - Gérard P. Huet (Theor. Comput. Sci., 2002)

Automata Mista. - Gérard P. Huet (Verification: Theory and Practice, 2003)

Zen and the Art of Symbolic Computing: Light and Fast Applicative Algorithms for Computational Linguistics. - Gérard P. Huet (PADL, 2003)

Special issue on 'Logical frameworks and metalanguages'. - Gérard P. Huet (J. Funct. Program., 2003)

A functional toolkit for morphological and phonological processing, application to a Sanskrit tagger. - Gérard P. Huet (J. Funct. Program., 2005)

The Reactive Engine for Modular Transducers. - Gérard P. Huet; Benoît Razet (Essays Dedicated to Joseph A. Goguen, 2006)

Shallow syntax analysis in Sanskrit guided by semantic nets constraints. - Gérard P. Huet (IWRIDL, 2006)

Formal Structure of Sanskrit Text: Requirements Analysis for a Mechanical Sanskrit Processor. - Gérard P. Huet (Sanskrit Computational Linguistics, 2008)

Preface. - Gérard P. Huet (Math. Struct. Comput. Sci., 2011)

A Distributed Platform for Sanskrit Processing. - Pawan Goyal 002; Gérard P. Huet; Amba P. Kulkarni; Peter M. Scharf; Ralph Bunker (COLING, 2012)

Sanskrit Linguistics Web Services. - Gérard P. Huet; Amba P. Kulkarni (COLING (Demos), 2014)

30 years of research and development around Coq. - Gérard P. Huet; Hugo Herbelin (POPL, 2014)

Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization. - Gérard P. Huet (FSCD, 2016)

Design and analysis of a lean interface for Sanskrit corpus annotation. - Pawan Goyal 002; Gérard P. Huet (J. Lang. Model., 2016)

Obituary Maurice Nivat (1937-2017). - Pierre-Louis Curien; Gérard P. Huet; Antoine Petit 001 (Bull. EATCS, 2017)

Computing with relational machines. - Gérard P. Huet; Benoît Razet (Math. Struct. Comput. Sci., 2017)