Gérard P. Huet

Gérard P. Huet's AcademicInfluence.com Rankings

Gérard P. Huet

Computer Science

#6573

World Rank

#6930

Historical Rank

Database

#3658

World Rank

#3809

Historical Rank

computer-science Degrees

Download Badge

Computer Science

Gérard P. Huet's Degrees

PhD Computer Science Paris-Saclay University

Similar Degrees You Can Earn

Best Online PhD of Computer Science (Doctorates) 2026

Why Is Gérard P. Huet Influential?

(Suggest an Edit or Addition)

(See a Problem?)

Gérard P. Huet's Published Works

Number of citations in a given year to any of this author's works

Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author

Published Works

The Calculus of Constructions (1988) (1345)
Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems (1980) (1153)
The Coq proof assistant : reference manual, version 6.1 (1997) (1109)
The coq proof assistant reference manual (2000) (1064)
Equations and rewrite rules: a survey (1980) (786)
Conflunt reductions: Abstract properties and applications to term rewriting systems (1977) (717)
A Unification Algorithm for Typed lambda-Calculus (1975) (475)
Proofs by induction in equational theories with constructors (1980) (371)
The Zipper (1997) (337)
The Coq proof assistant user's guide : version 5.6 (1990) (327)
Constructions: A Higher Order Proof System for Mechanizing Mathematics (1985) (249)
On the Uniform Halting Problem for Term Rewriting Systems (1978) (230)
Programming Environments Based on Structured Editors: The MENTOR Experience, (1980) (224)
A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm (1981) (206)
Computations in Orthogonal Rewriting Systems, I (1991) (170)
Computations in Orthogonal Rewriting Systems, II (1991) (167)
The Coq Proof Assistant A Tutorial (2005) (153)
The Undecidability of Unification in Third Order Logic (1973) (144)
Proving and applying program transformations expressed with second-order patterns (1978) (115)
Complete Sets of Unifiers and Matchers in Equational Theories (1983) (114)
The Coq Proof Assistant : A Tutorial : Version 7.2 (1997) (112)
Constrained resolution: a complete method for higher-order logic. (1972) (95)
A Mechanization of Type Theory (1973) (88)
An Algorithm to Generate the Basis of Solutions to Homogeneous Linear Diophantine Equations (1978) (86)
Residual theory in λ-calculus: a formal development (1994) (84)
A functional toolkit for morphological and phonological processing, application to a Sanskrit tagger (2005) (75)
Constructive category theory (2000) (70)
Formal structures for computation and deduction (1986) (65)
Logical Foundations of Functional Programming (1990) (64)
Logical frameworks (1991) (53)
The Constructive Engine (1989) (43)
Shallow syntax analysis in Sanskrit guided by semantic nets constraints (2006) (40)
A Distributed Platform for Sanskrit Processing (2012) (39)
A uniform approach to type theory (1990) (37)
Formal Structure of Sanskrit Text: Requirements Analysis for a Mechanical Sanskrit Processor (2009) (35)
Induction Principles Formalized in the Calculus of Constructions (1987) (33)
Cartesian closed Categories and Lambda- calculus (1985) (28)
Deduction and Computation (1985) (28)
Towards Computational Processing of Sanskrit (2003) (26)
Design and analysis of a lean interface for Sanskrit corpus annotation (2016) (25)
The zen computational linguistics toolkit (2002) (24)
Lexicon-directed segmentation and tagging in Sanskrit (2003) (24)
Sanskrit Computational Linguistics (2009) (22)
Completeness Analysis of a Sanskrit Reader (2012) (21)
Higher Order Unification 30 Years Later (2002) (21)
Design of a Lexical Database for Sanskrit (2004) (20)
The Reactive Engine for Modular Transducers (2006) (19)
Unification in Typed Lambda Calculus (1975) (18)
An Analysis of Böhm's Theorem (1993) (18)
Linear Contexts and the Sharing Functor: Techniques for Symbolic Computation (2002) (14)
Zen and the Art of Symbolic Computing: Light and Fast Applicative Algorithms for Computational Linguistics (2003) (13)
From an informal textual lexicon to a well-structured lexical database: an experiment in data reverse engineering (2001) (12)
30 years of research and development around Coq (2014) (11)
Special issue on ‘Logical frameworks and metalanguages’ (2003) (8)
The Gallina Specification language: A Case Study (1992) (8)
Introduction au λ-calcul pur (1991) (7)
The Calculus of Constructions: State of the Art (1987) (7)
The Gilbreath Trick : A case study in Axiomatisation and Proof Development in the Coq Proof (1991) (7)
Papers presented at the second annual Workshop on Logical environments (1993) (7)
Extending the Calculus of Constructions with Type:Type (2004) (6)
A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction (1985) (6)
Preliminary Design of a Sanskrit Corpus Manager (2018) (5)
Regular Böhm trees (1998) (5)
Computing with relational machines (2015) (5)
Validation and Normalization of DCS corpus using Sanskrit Heritage tools to build a tagged Gold Corpus (2020) (4)
Sanskrit Linguistics Web Services (2014) (4)
Design of a proof assistant (1996) (3)
Linear Contexts, Sharing Functors: Techniques for Symbolic Computation (2003) (3)
Finite-State Transducers as Regular Böhm Trees (1997) (3)
Equational systems for category theory and intuitionistic logic (1985) (3)
Sanskrit Computational Linguistics, First and Second International Symposia Rocquencourt, France, October 29-31, 2007 Providence, RI, USA, May 15-17, 2008 Revised Selected and Invited Papers (2009) (3)
In Defense of Programming Languages Design (1982) (2)
Srl Yantra Geometry (2002) (2)
Internet challenges for informatics research (2005) (2)
A Collaborative Platform for Sanskrit Processing (2012) (2)
Theorem Proving Systems of the Formel Project (1986) (2)
Axiomatisations, Proofs, and Formal Specifications of Algorithms: Commented Case Studies in the Coq Proof Assistant (1997) (2)
Sanskrit signs and Pān. inian scripts (2015) (2)
Sanskrit computational linguistics : third international symposium, Hyderabad, India, January 15-17, 2009 : proceedings (2009) (2)
Design Proof Assistant (Abstract) (1996) (1)
Logical Frameworks: Introduction (1991) (1)
Higher order unification 30 years later: (Extended abstract) (2002) (1)
Specifications, Algorithms, Axiomatisations and Proofs - Commented Case Studies In the Coq Proof Ass (1995) (1)
Obituary Maurice Nivat (1937-2017) (2017) (0)
Validation and Normalization of DCS corpus and Development of the Sanskrit Heritage Engine’s Segmenter (2023) (0)
Proceedings of the 3rd International Symposium on Sanskrit Computational Linguistics (2008) (0)
Improved microcircuit card reader (1989) (0)
A constructive denotational semantics for Kahn networks in Coq (2019) (0)
Scientific Foundations - Discourse and dialogue structure: computational semantics and pragmatics (2005) (0)
In defence of programming language design (1985) (0)
New Results - Parsers (2007) (0)
LCF formalism ● In 1969 , the LCF ( ' Logic for computable functions ' ) formalism was devised by Dana Scott (2018) (0)
Joint team: Sanskrit Computational Linguistics Three-year evaluation document Creation date: 1-1-07 Consortium partners (2009) (0)
Scientific Foundations - Word structure and automata: computational morphology (2006) (0)
New Results - Computational linguistics (2005) (0)
Artificial Intelligence in Western Europe (1977) (0)
Linguistic signs, grammar and meaning: computational logic for natural language (2006) (0)
Sanskrit lexicography, past and future (2019) (0)
Program semantics and infinite regular terms (2009) (0)
Scientific Foundations - Type systems and functional programming for computational linguistics (2007) (0)
Mechanizing Constructive Proofs (Abstract) (1986) (0)
Initiation au Lambda-Calcul (An Initiation into Lambda Calculus) (1989) (0)
From Semantics to Computer Science: Preface (2009) (0)
The future of symbolic computation: mathematics versus languages (1984) (0)
Logical Frameworks: Preface (1991) (0)
Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization (2016) (0)
A crash course in λ-calculus (1998) (0)
Special Issue: Interactive Theorem Proving and the Formalisation of Mathematics Guest Editors: Andrea Asperti and Jeremy Avigad Preface (2011) (0)
Preface (2011) (0)
Software - Prototype software (2005) (0)
Design Issues for a Computer-aided Environment for Constructive Mathematics (Abstract) (1990) (0)
Sanskrit Heritage Site (2014) (0)