default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDGérard P. Huet
Person information
- affiliation: INRIA, France
- award (2013): ACM Software System Award
- award (1998): Herbrand Award
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2010 – 2019
- 2017
[j22]Pierre-Louis Curien, Gérard P. Huet, Antoine Petit:
Obituary Maurice Nivat (1937-2017). Bull. EATCS 123 (2017)- [j21]Gérard P. Huet, Benoît Razet:
Computing with relational machines. Math. Struct. Comput. Sci. 27(5): 807-826 (2017) - 2016
- [j20]Pawan Goyal, Gérard P. Huet:
Design and analysis of a lean interface for Sanskrit corpus annotation. J. Lang. Model. 4(2): 145-182 (2016) - [c33]Gérard P. Huet:
Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization. FSCD 2016: 3:1-3:2 - 2014
- [c32]Gérard P. Huet, Amba P. Kulkarni
:
Sanskrit Linguistics Web Services. COLING (Demos) 2014: 48-51 - [c31]Gérard P. Huet, Hugo Herbelin:
30 years of research and development around Coq. POPL 2014: 249-250 - 2012
- [c30]Pawan Goyal, Gérard P. Huet, Amba P. Kulkarni, Peter M. Scharf, Ralph Bunker:
A Distributed Platform for Sanskrit Processing. COLING 2012: 1011-1028 - 2011
- [j19]Gérard P. Huet:
Preface. Math. Struct. Comput. Sci. 21(4): 671-677 (2011)
2000 – 2009
- 2009
- [e2]Gérard P. Huet, Amba P. Kulkarni, Peter M. Scharf:
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. Lecture Notes in Computer Science 5402, Springer 2009, ISBN 978-3-642-00154-3 [contents] - [e1]Amba P. Kulkarni, Gérard P. Huet:
Sanskrit Computational Linguistics, Third International Symposium, Hyderabad, India, January 15-17, 2009. Proceedings. Lecture Notes in Computer Science 5406, Springer 2009, ISBN 978-3-540-93884-2 [contents] - 2008
- [c29]Gérard P. Huet:
Formal Structure of Sanskrit Text: Requirements Analysis for a Mechanical Sanskrit Processor. Sanskrit Computational Linguistics 2008: 162-199 - 2006
- [c28]Gérard P. Huet, Benoît Razet:
The Reactive Engine for Modular Transducers. Essays Dedicated to Joseph A. Goguen 2006: 355-374 - [c27]Gérard P. Huet:
Shallow syntax analysis in Sanskrit guided by semantic nets constraints. IWRIDL 2006: 6 - 2005
- [j18]Gérard P. Huet:
A functional toolkit for morphological and phonological processing, application to a Sanskrit tagger. J. Funct. Program. 15(4): 573-614 (2005) - 2003
- [j17]Gérard P. Huet:
Special issue on 'Logical frameworks and metalanguages'. J. Funct. Program. 13(2): 257-260 (2003) - [c26]Gérard P. Huet:
Automata Mista. Verification: Theory and Practice 2003: 359-372 - [c25]Gérard P. Huet:
Zen and the Art of Symbolic Computing: Light and Fast Applicative Algorithms for Computational Linguistics. PADL 2003: 17-18 - 2002
- [j16]Gérard P. Huet:
Srl Yantra Geometry. Theor. Comput. Sci. 281(1-2): 609-628 (2002) - [c24]Gérard P. Huet:
Higher Order Unification 30 Years Later. TPHOLs 2002: 3-12 - 2001
- [c23]Gérard P. Huet:
From an Informal Textual Lexicon to a Well-Structured Lexical Database: An Experiment in Data Reverse Engineering. WCRE 2001: 127-135 - 2000
- [c22]Gérard P. Huet, Amokrane Saïbi:
Constructive category theory. Proof, Language, and Interaction 2000: 239-276
1990 – 1999
- 1998
- [j15]Gérard P. Huet:
Regular Böhm trees. Math. Struct. Comput. Sci. 8(6): 671-680 (1998) - 1997
- [j14]Gérard P. Huet:
The Zipper. J. Funct. Program. 7(5): 549-554 (1997) - [c21]Gérard P. Huet, Henri Laulhère:
Finite-State Transducers as Regular Böhm Trees. TACS 1997: 604-610 - 1996
- [c20]Gérard P. Huet:
Design Proof Assistant (Abstract). RTA 1996: 153 - 1994
- [j13]Gérard P. Huet:
Residual Theory in lambda-Calculus: A Formal Development. J. Funct. Program. 4(3): 371-394 (1994) - 1993
- [j12]Gérard P. Huet:
An Analysis of Böhm's Theorem. Theor. Comput. Sci. 121(1&2): 145-167 (1993) - 1992
- [c19]Gérard P. Huet:
The Gallina Specification language: A Case Study. FSTTCS 1992: 229-240 - 1991
- [c18]Gérard P. Huet, Jean-Jacques Lévy:
Computations in Orthogonal Rewriting Systems, I. Computational Logic - Essays in Honor of Alan Robinson 1991: 395-414 - [c17]Gérard P. Huet, Jean-Jacques Lévy:
Computations in Orthogonal Rewriting Systems, II. Computational Logic - Essays in Honor of Alan Robinson 1991: 415-443 - 1990
- [c16]Gérard P. Huet:
Design Issues for a Computer-aided Environment for Constructive Mathematics (Abstract). DISCO 1990: 55
1980 – 1989
- 1989
- [p1]Gérard P. Huet:
The Constructive Engine. A Perspective in Theoretical Computer Science 1989: 38-69 - 1988
- [j11]Thierry Coquand, Gérard P. Huet:
The Calculus of Constructions. Inf. Comput. 76(2/3): 95-120 (1988) - 1987
- [c15]Gérard P. Huet:
The Calculus of Constructions: State of the Art. FSTTCS 1987: 372 - [c14]Gérard P. Huet:
Induction Principles Formalized in the Calculus of Constructions. TAPSOFT, Vol.1 1987: 276-286 - 1986
- [j10]François Fages, Gérard P. Huet:
Complete Sets of Unifiers and Matchers in Equational Theories. Theor. Comput. Sci. 43: 189-200 (1986) - [c13]Gérard P. Huet:
Mechanizing Constructive Proofs (Abstract). CADE 1986: 403 - [c12]Gérard P. Huet:
Theorem Proving Systems of the Formel Project. CADE 1986: 687-688 - 1985
- [j9]Thierry Coquand, Gérard P. Huet:
A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction. J. Symb. Comput. 1(3): 323-328 (1985) - [c11]Gérard P. Huet:
Deduction and Computation. Advanced Course: Fundamentals of Artificial Intelligence 1985: 38-74 - [c10]Thierry Coquand, Gérard P. Huet:
Constructions: A Higher Order Proof System for Mechanizing Mathematics. European Conference on Computer Algebra (1) 1985: 151-184 - [c9]Gérard P. Huet:
Cartesian closed Categories and Lambda- calculus. Combinators and Functional Programming Languages 1985: 123-135 - [c8]Thierry Coquand, Gérard P. Huet:
Concepts mathématiques et informatiques formalisés dans le calcul des constructions. Logic Colloquium 1985: 123-146 - 1984
- [j8]Gérard P. Huet:
The future of symbolic computation: mathematics versus languages. SIGSAM Bull. 18(2): 2-5 (1984) - 1983
- [c7]François Fages, Gérard P. Huet:
Complete Sets of Unifiers and Matchers in Equational Theories. CAAP 1983: 205-220 - 1982
- [j7]Gérard P. Huet, Jean-Marie Hullot:
Proofs by Induction in Equational Theories with Constructors. J. Comput. Syst. Sci. 25(2): 239-266 (1982) - [c6]Gérard P. Huet:
In Defense of Programming Languages Design. ECAI 1982: 19-27 - 1981
- [j6]Gérard P. Huet:
A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm. J. Comput. Syst. Sci. 23(1): 11-21 (1981) - 1980
- [j5]Gérard P. Huet:
Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems. J. ACM 27(4): 797-821 (1980) - [c5]Gérard P. Huet, Jean-Marie Hullot:
Proofs by Induction in Equational Theories with Constructors. FOCS 1980: 96-107
1970 – 1979
- 1978
- [j4]Gérard P. Huet, Bernard Lang:
Proving and Applying Program Transformations Expressed with Second-Order Patterns. Acta Informatica 11: 31-55 (1978) - [j3]Gérard P. Huet:
An Algorithm to Generate the Basis of Solutions to Homogeneous Linear Diophantine Equations. Inf. Process. Lett. 7(3): 144-147 (1978) - 1977
- [c4]Gérard P. Huet:
Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. FOCS 1977: 30-45 - [c3]Jacques Pitrat, Erik Sandewall, Wolfgang Bibel, Gérard P. Huet, Hans-Hellmut Nagel, M. Somalivco:
Artificial Intelligence in Western Europe. IJCAI 1977: 955-969 - 1975
- [j2]Gérard P. Huet:
A Unification Algorithm for Typed lambda-Calculus. Theor. Comput. Sci. 1(1): 27-57 (1975) - [c2]Gérard P. Huet:
unification in typed lambda calculus. Lambda-Calculus and Computer Science Theory 1975: 192-212 - 1973
- [j1]Gérard P. Huet:
The Undecidability of Unification in Third Order Logic. Inf. Control. 22(3): 257-267 (1973) - [c1]Gérard P. Huet:
A Mechanization of Type Theory. IJCAI 1973: 139-146
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-01-09 13:24 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
