Suivre
Gérard Huet
Gérard Huet
Directeur de Recherche Emérite Inria
Adresse e-mail validée de inria.fr - Page d'accueil
Titre
Citée par
Citée par
Année
The calculus of constructions
T Coquand, G Huet
INRIA, 1986
19741986
Confluent reductions: Abstract properties and applications to term rewriting systems
G Huet
18th Annual Symposium on Foundations of Computer Science (sfcs 1977), 30-45, 1977
1724*1977
Equations and rewrite rules. A Survey. In “Formal languages: perspectives an open problems”
G Huet, D Oppen
Academic Press, 1980
1192*1980
A unification algorithm for typed λ-calculus
GP Huet
Theoretical Computer Science 1 (1), 27-57, 1975
9731975
Résolution d’équations dans les langages d’ordre 1, 2,..., ω, 1976
G Huet
These d’État, Université Paris 7, 0
679*
The Zipper
G Huet
J. functional programming 7 (5), 549-554, 1997
4631997
Proofs by induction in equational theories with constructors
G Huet, JM Hullot
Journal of computer and system sciences 25 (2), 239-266, 1982
4611982
Proving and applying program transformations expressed with second-order patterns
G Huet, B Lang
Acta informatica 11 (1), 31-55, 1978
4431978
Computations in Orthogonal Rewriting Systems, II.
GP Huet, JJ Lévy
Computational Logic-Essays in Honor of Alan Robinson, 415-443, 1991
4021991
Constructions: A higher order proof system for mechanizing mathematics
T Coquand, G Huet
EUROCAL'85: European Conference on Computer Algebra Linz, Austria, April 1–3 …, 2005
3662005
Programming environments based on structured editors: The MENTOR experience
V Donzeau-Gouge, G Huet, G Kahn, B Lang
INSTITUT NATIONAL DE RECHERCHE D'INFORMATIQUE ET D'AUTOMATIQUE ROCQUENCOURT …, 1980
3571980
A complete proof of correctness of the Knuth-Bendix completion algorithm
G Huet
Journal of Computer and System Sciences 23 (1), 11-21, 1981
3201981
On the uniform halting problem for term rewriting systems
G Huet
INRIA Technical Report 283, 1978
3161978
The Coq proof assistant reference manual: Version 6.1
B Barras, S Boutin, C Cornes, J Courant, JC Filliatre, E Gimenez, ...
Inria, 1997
3151997
Call by need computations in non-ambiguous linear term rewriting systems
G Huet
Technical Report 359, 1979
2031979
The undecidability of unification in third order logic
GP Huet
Information and control 22 (3), 257-267, 1973
1901973
The coq proof assistant a tutorial
G Huet, G Kahn, C Paulin-Mohring
Rapport Technique 178, 1997
169*1997
Constrained resolution: a complete method for higher-order logic.
GP Huet
Case Western Reserve University, 1972
148*1972
The Coq proof assistant user's guide: version 5.8
G Dowek, A Felty, H Herbelin, G Huet, C Parent, C Paulin-Mohring, ...
INRIA, 1993
1331993
The Coq proof assistant reference manual
B Barras, S Boutin, C Cornes, J Courant, Y Coscoy, D Delahaye, ...
INRIA, version 6 (11), 1999
1131999
Le système ne peut pas réaliser cette opération maintenant. Veuillez réessayer plus tard.
Articles 1–20