| The calculus of constructions T Coquand, G Huet INRIA, 1986 | 1974 | 1986 |
| 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 | 973 | 1975 |
| 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 | 463 | 1997 |
| Proofs by induction in equational theories with constructors G Huet, JM Hullot Journal of computer and system sciences 25 (2), 239-266, 1982 | 461 | 1982 |
| Proving and applying program transformations expressed with second-order patterns G Huet, B Lang Acta informatica 11 (1), 31-55, 1978 | 443 | 1978 |
| Computations in Orthogonal Rewriting Systems, II. GP Huet, JJ Lévy Computational Logic-Essays in Honor of Alan Robinson, 415-443, 1991 | 402 | 1991 |
| 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 | 366 | 2005 |
| 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 | 357 | 1980 |
| A complete proof of correctness of the Knuth-Bendix completion algorithm G Huet Journal of Computer and System Sciences 23 (1), 11-21, 1981 | 320 | 1981 |
| On the uniform halting problem for term rewriting systems G Huet INRIA Technical Report 283, 1978 | 316 | 1978 |
| The Coq proof assistant reference manual: Version 6.1 B Barras, S Boutin, C Cornes, J Courant, JC Filliatre, E Gimenez, ... Inria, 1997 | 315 | 1997 |
| Call by need computations in non-ambiguous linear term rewriting systems G Huet Technical Report 359, 1979 | 203 | 1979 |
| The undecidability of unification in third order logic GP Huet Information and control 22 (3), 257-267, 1973 | 190 | 1973 |
| 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 | 133 | 1993 |
| The Coq proof assistant reference manual B Barras, S Boutin, C Cornes, J Courant, Y Coscoy, D Delahaye, ... INRIA, version 6 (11), 1999 | 113 | 1999 |
Christine PAULIN-MOHRINGLMF, Université Paris-SaclayAdresse e-mail validée de universite-paris-saclay.fr
