Publications of Gérard Huet

[115]
Gérard Huet and Amba Kulkarni, eds.

Computational Sanskrit and Digital Humanities.
DK Publishers, Delhi, 2018.

[114]
Gérard Huet and Idir Lankri.

Preliminary Design of a Sanskrit Corpus Manager.
17th World Sanskrit Conference, Vancouver, July 2018.
Available electronically as

pdf.
Final version in [115].

[113]
Gérard Huet.

Le sanskrit et les mathématiques.
Maths Langages Express, Comité international des jeux
mathématiques, Paris, Mai 2017.
Available electronically as

pdf.

[112]
Gérard Huet.

Sanskrit signs and Pāṇinian scripts.
16th World Sanskrit Conference, Bangkok, July 2015.
Available electronically as

pdf.
Final version in Sanskrit and Computational Linguistics, ed. Amba Kulkarni,
D.K. Publishers, New Delhi, India, 2016, pp 53-76.

[111]
Pawan Goyal and Gérard Huet.

Design and analysis of a lean interface for
Sanskrit corpus annotation.
Extended version of [108].

Journal of Linguistic Modeling, Vol 4, No 2, 2016.

[110]
Gérard Huet.

Fondements de l'informatique, à la croisée des
mathématiques, de la logique et de la linguistique.
Colloque sur l'enseignement philosophique et les sciences,
Fondation Simone et Cino Del Duca, 13 novembre 2013.
Available electronically as

docx.

[109]
Gérard Huet and Pawan Goyal.

Design of a lean interface for Sanskrit corpus annotation.
Proceedings, ICON13, Hyderabad December 2013.
Available electronically as

pdf.

[108]
Gérard Huet and Benoît Razet.

Computing with Relational Machines.
Mathematical Structures in Computer Science, special issue
in honor of Corrado Böhm, October 2015.
Available electronically as

pdf.
Final version at

Cambridge
University Press.

[107]
Pawan Goyal and Gérard Huet.

Completeness Analysis of a Sanskrit Reader.
Proceedings of the Fifth International Symposium on Sanskrit Computational
Linguistics, Mumbai, January 2013.
Available electronically as

pdf.
Final version in "Recent Researches in Sanskrit Computational Linguistics",
Ed. Malhar Kulkarni and Chaitali Dangarikar, D.K. Printworld, 2013.

[106]
Pawan Goyal and Gérard Huet and Amba Kulkarni and Peter Scharf and
Ralph Bunker.

A Distributed Platform for Sanskrit Processing.
24th International Conference on Computational Linguistics, Mumbai,
December 2012. Available electronically at

aclweb.

[105]
G. Huet.

Departing from Pāṇini for good reasons.
15th World Sanskrit Conference, New Delhi, January 2012.
Abstract available electronically as

pdf.

[104]
G. Huet.

Preface.
Special Issue: Interactive Theorem Proving and the Formalisation of Mathematics.
Math. Struct. in Comp. Science (2011) vol. 21, pp. 671-677, Cambridge
University Press.
Available electronically as

pdf.

[103]
G. Huet.

Sanskrit Segmentation.
South Asian Languages Analysis Roundtable XXVIII, Denton, Texas. October 2009.
Available electronically as

pdf.

[102]
Y. Bertot, G. Huet, J.J. Lévy & G. Plotkin, Eds.

From Semantics to Computer Science. Essays in Honour of Gilles Kahn.
Cambridge University Press, 2009.

[101]
G. Huet & A. Kulkarni, Eds.

Sanskrit Computational Linguistics 3.
Springer-Verlag Lecture Notes 5406, 2009.

[100]
G. Huet, A. Kulkarni & P. Scharf, Eds.

Sanskrit Computational Linguistics 1 and 2.
Springer-Verlag Lecture Notes 5402, 2009.

[99]
G. Huet et B. Razet.

Calculs applicatifs de machines relationnelles.
Journées Francophones des Langages Applicatifs (JFLA), Saint Quentin sur Isère, Janvier 2009.
Available electronically as

pdf.

[98]
G. Huet and B. Razet.

Computing with Relational Machines.
ICON'2008 Tutorial, Pune, December 2008.
Available electronically as

pdf.

[97]
G. Huet.

Automates, machines, moteurs réactifs.
Notes de cours, Master Parisien de Recherche en Informatique, Automne 2008.
Available electronically as

pdf.

[96]
G. Huet.

Formal structure of Sanskrit text:
Requirements analysis for a mechanical Sanskrit processor.
Proceedings,
Second International Symposium on Sanskrit Computational Linguistics,
Ed. Peter Scharf,
Brown University, Providence, May 2008.
Final version in “Topics in Sanskrit Computational Linguistics”,
Eds. G. Huet, A. Kulkarni & P. Scharf, Springer-Verlag Lecture Notes 5402, 2009.
Available electronically as

pdf.

[95]
G. Huet.

Shallow syntax analysis in Sanskrit guided by semantic nets constraints.
Proceedings of International Workshop on Research Issues in Digital Libraries, Kolkata, Dec. 2006.
Editors Prasenjit Majumder, Mandar Mitra and Swapan K. Parui, ACM Digital Library.
Available electronically as

pdf.

[94]
G. Huet.

Vérité Mathématique, cohérence logique et vérification informatique.
Conference transcript in Science et Devenir de l'Homme,
les cahiers du M.U.R.S. 49, 3ème trimestre 2006, pub. Mouvement Universel de la
Responsabilité Scientifique, Paris, pp. 42-61.
Available electronically

here.

[93]
G. Huet and B. Razet.

The Reactive Engine for Modular Transducers.
In Algebra, Meaning and Computation, Essays Dedicated to Joseph A. Goguen
on the Occasion of His 65th Birthday. Kokichi Futatsugi, Jean-Pierre
Jouannaud and José Meseguer Eds.
Springer LNCS 4060, 2006, pp. 355-374.
Available electronically as

pdf.

[92]
G. Huet.

Internet Challenges for Informatics Research.
Progress in Informatics No 2, Nov. 2005, National Institute of Informatics,
Tokyo, Japan, pp. 355-374.
Available electronically as

pdf.

[91]
Ph. Flajolet and G. Huet.

Mathématiques et informatique.
Chapter in “Les mathématiques dans le monde contemporain”,
Ed. Jean-Christophe Yoccoz,
Rapport sur la science et la technologie n. 20,
Académie des sciences, 2005.
Available electronically as

doc.

[90]
G. Huet.

Design of a Lexical Database for Sanskrit.
COLING Workshop on Electronic Dictionaries, Geneva, Aug. 29th, 2004,
pp. 8-14.
Available electronically as

pdf.

[89]
G. Huet.

Towards Computational Processing of Sanskrit.
ICON-2003, Mysore, India, Dec. 2003.
Proceedings Eds. Rajeev Sangal, S. M. Bendre and Udaya Narayana Singh,
Central Institute of Indian Languages, Mysore, pp. 40-48.
Available electronically as

pdf.

[88]
G. Huet.

Lexicon-directed Segmentation and Tagging of Sanskrit.
XIIth World Sanskrit Conference, Helsinki, Finland, Aug. 2003.
Final version in

Themes and Tasks in Old and Middle Indo-Aryan Linguistics,
Eds. Bertil Tikkanen & Heinrich Hettrich. Motilal Banarsidass, Delhi, 2006, pp. 307-325.
Available electronically as

pdf.

[87]
G. Huet.

Automata Mista.
Festschrift in Honor of Zohar Manna for his 64th anniversary,
Taormina, Sicily, July 2003.
In “Verification: Theory and Practice: Essays Dedicated
to Zohar Manna on the Occasion of His 64th Birthday”,
Ed. Nachum Dershowitz, Springer-Verlag LNCS vol. 2772, pp. 359-372.
Available electronically as

pdf.

[86]
G. Huet.

Zen and the Art of Symbolic Computing: Light and Fast Applicative Algorithms for Computational Linguistics.
Invited conference, Practical Aspects of Declarative Languages (PAdl)
symposium, New Orleans, Jan. 2003.
Abstract available as

pdf.
Slides available as

pdf.

[85]
G. Huet.

The Zen Computational Linguistics Toolkit:
Lexicon Structures and Morphology Computations using a Modular
Functional Programming Language.
Tutorial, Language Engineering Conference LEC'2002, Hyderabad.

pdf.

[84]
G. Huet.

Constructive Computation Theory.
Course notes on lambda calculus, University of Bordeaux I, 2002.
Available electronically as

pdf.
Executable Objective Caml library available as

gzipped tar archive.

[83]
G. Huet.

The Zen Computational Linguistics Toolkit.
ESSLLI 2002 Lectures, Trento, Italy, Aug. 2002.
Available electronically as

pdf.
Slides available as

pdf.

[82]
G. Huet.

Śrī Yantra Geometry.
Theoretical Computer Science 281 (2002) pp. 609-628.
Available electronically as

ps
and

pdf.
This study was used for the design of the anniversary volume

cover.

[81]
G. Huet.

Higher Order Unification 30 years later.
Proceedings, 15th International Conference TPHOL 2002.
Eds V. Carreño, C. Muñoz and S. Tahar.
LNCS 2410, pp. 3-12.
Available electronically as

ps.
Slides available as

pdf.

[80]
G. Huet.

Linear Contexts and the Sharing Functor:
Techniques for Symbolic Computation.
Workshop on Thirty Five Years of Automath,
Heriot-Watt University, Edinburgh, April 2002.
Slides available as

ps.
Final version in

**Thirty Five Years of Automating
Mathematics**, ed. Fairouz Kamareddine, Kluwer 2003.
Available electronically as

pdf.

[79]
G. Huet.

A Functional Toolkit for Morphological and Phonological Processing, Application to a Sanskrit Tagger.
Journal of Functional Programming

**15** (4) pp. 573-614, 2005.
Preliminary version available electronically as

postscript
or

pdf.

[78]
G. Huet.

Computational Tools for Sanskrit.
Workshop on Computational Linguistics in South Asian Languages,
XXIth South Asian Languages Analysis Roundatable, University of Constanz,
Oct. 2001.

[77]
G. Huet.

Juncture Transducers.
Unpublished, 2001.

[76]
G. Huet.

From an informal textual lexicon to a well-structured lexical database: An experiment in data reverse engineering.
IEEE Working Conference on Reverse Engineering (WCRE’2001),
Stuttgart, Oct. 2001, pp. 127-135.
Available electronically as

pdf.

[75]
G. Huet.

Computational Linguistics for Sanskrit: a Software Engineering Approach.
Unpublished, 2001.

[74]
G. Huet.

Structure of a Sanskrit dictionary.
INRIA Technical Report, Sept. 2000.
Available as

postscript file.

[73]
G. Huet.

Structure of a Sanskrit dictionary.
XIth International Sanskrit Conference, Torino, April 2000.

[72]
G. Huet.

Programmes mobiles auto-certifiés : Principes généraux et mise en œuvre
des paquets auto-certifiants dans le système Coq.
Actes du 4ème Colloque Africain sur la Recherche en Informatique (CARI’98),
Ed. Maurice Tchuente, Presses Universitaires de Dakar, Sénégal (oct. 98),
pp. 17-21.

[71]
A. Chander and G. Huet.

Prooflets: A general paradigm for self-certifiable mobile code and its implementation in the Coq Proof Assistant.
Unpublished (1999).

[70]
G. Huet.

The Zipper.
J. Functional Programming,

**7** (5), Sept 1997, pp. 549-554.
Available as

pdf file.

[69]
G. Huet and H. Laulhère.

Finite-state Transducers as Regular Böhm Trees.
Theoretical Aspects of Computer Software, Eds. M. Abadi and T. Ito.
Springer-Verlag LNCS 1281, Sept. 97, pp. 604-610.
Available as

postscript file
and

pdf file.

[68]
G. Huet.

Regular Böhm Trees.
Math. Struct. in Comp. Science, 1998, vol. 8, pp. 671-680.
Available as

postscript file
and

pdf file.

[67]
G. Huet.

Design of a proof assistant.
Invited conference, XIth IEEE Conference on Logic in Computer Science,
New Brunswick, 1996.

[66]
G. Huet and A. Saïbi.

Constructive Category Theory.
CLICS-TYPES BRA meeting, Jan. 1995.
Final version published in

**Proof, Language and Interaction -
Essays in Honour of Robin Milner**.
Eds. Gordon Plotkin, Colin Stirling and Mads Tofte,
MIT Press, 2000.

[65]
G. Huet.

Specifications, Algorithms, Axiomatisations and Proofs.
Commented Case Studies in the Coq Proof Assistant.
Course Notes, Marktoberdorf School on Logic of Computation,
Aug. 1995.
Available electronically as

pdf.

[64]
G. Huet, G. Kahn and Ch. Paulin-Mohring.

The Coq Proof Assistant - A tutorial.
INRIA Technical Report 178, Juillet 1995.

[63]
C. Cornes, J. Courant, J.-C. Filliâtre,
G. Huet, P. Manoury, C. Muñoz, C. Murthy, C. Parent,
Ch. Paulin-Mohring, A. Saïbi, B. Werner.

The Coq Proof Assistant Reference Manual, Version 5.10.
INRIA Technical Report 177, Juillet 1995.

[62]
G. Dowek, G. Huet and B. Werner.

On the Definition of the η-long Normal Form in the Type Systems of the Cube.
Informal Proceedings of the Workshop "Types", Nijmegen, 1993.

[61]
G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring and B. Werner.

The Coq Proof Assistant User’s Guide. Version 5.8.
INRIA Technical Report 154, Mai 1993.

[60]
Gérard Huet. Certification du logiciel : Méthodes et outils.

Etat de l’art des méthodes formelles en génie logiciel.
Rapport 11/SGDN/STS/VST, SGDN, 1994.

[59]
Gérard Huet and Gordon Plotkin, eds.

Logical Environments.
Cambridge University Press, 1993.

[58]
G. Huet.

Residual Theory in λ-calculus:
A Formal Development.
Rapport de Recherche INRIA No 2009, Août 93.
Also Journal of Functional Programming (4,3) pp. 371-394, 1994.
Available electronically as

pdf.

[57]
G. Huet.

An analysis of Böhm's theorem.
Rapport de Recherche INRIA No 2008, Août 93.
Also in

To C. Böhm: Essays on Lambda-Calculus and Functional
Programming,
eds. M. Dezani-Ciancaglini, S. Ronchi della Rocca and M. Venturini Zilli.
Also Theoretical Computer Science 121 (1993) 145-167.
Available electronically as

pdf.

[56]
G. Huet.

The Gallina specification language : A case study.
Proceedings of 12th FST/TCS Conference, New Delhi, Dec. 1992.
Ed. R. Shyamasundar, Springer Verlag LNCS 652, 229-240.

[55]
G. Huet.

Constructive Computation Theory, Part I.
Course Notes, DEA Informatique, Mathématiques et Applications,
Paris, Oct. 1992.
Final version, with executable library of ML code, listed above as [84].

[54]
Gérard Huet and Gordon Plotkin, eds.

Logical Frameworks.
Cambridge University Press, 1991.

[53]
G. Huet, J.J. Lévy.

Call by Need Computations in Orthogonal Term Rewriting Systems.
In Computational Logic,
J.A. Robinson anniversary volume, J. L. Lassez and G. Plotkin Eds,
MIT Press, 1991.

[52]
G. Huet.

Initiation au λ-calcul.
These notes in French correspond to courses on λ-calcul I gave in the
DEA "Fonctionnalité, Structures de Calcul et Programmation" at Université
Paris VII from 1987 to 1991. They subsume both [43] and [51], covering both
untyped and typed λ-calcul. They were composed in MacWrite on a
Macintosh SE-30 and bound as an A-8 document.
In 2018 they were re-scanned to produce an enormous (50Mb)
un-searcheable

pdf document.

[51]
G. Huet.

Introduction au λ-calcul typé.
In Logique et Informatique : une introduction",
Ed. Bruno Courcelle,
Collection Didactique, INRIA, 1991.

[50]
G. Huet.

The Gilbreath trick: A case study in axiomatisation and proof development in the Coq Proof Assistant.
Proceedings, Second Workshop on Logical Frameworks, Edinburgh, May 1991.
Rapport de recherche INRIA 1511, Sept. 1991.
Available electronically as

pdf.

[49]
G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Paulin, B. Werner.

The Coq Proof Assistant User's Guide, Version 5.6.
INRIA Technical Report 134, Dec. 1991.

[48]
G. Huet, Editor.

Logical Foundations of Functional Programming.
Addison-Wesley, 1990.

[47]
G. Huet.

A higher-order proof system for machine-aided development of verified
software.
Invited talk, ICMIDC, Symposium on Mathematics of Computation,
Ho Chi Minh City, April 88.

[46]
G. Huet.

An Overview of the Calculus of Constructions.
Invited talk, The Logic Programming Conference 88, Tokyo, April 88.

[45]
G. Huet.

Experiments with GHC prototypes.
Technical note, ICOT, Tokyo, May 1988. Available in the following pdf

unpublished report.

[44]
G. Huet.

The Constructive Engine. Version 4.5.
Invited Conference, 2nd European Symposium on Programming, Nancy, March 88.
Final version in anniversary volume

**Theoretical Computer Science** in memory of Gift Siromoney, Ed. R. Narasimhan,
World Scientific Publishing, 1989.
Available electronically as

pdf.

[43]
G. Huet.

Initiation à la Calculabilité.
Notes de cours du DEA

Fonctionnalité, Structures de Calcul et
Programmation, Université Paris 7, Jan. 88.

[42]
G. Huet.

The Calculus of Constructions: State of the Art.
Invited Conference, Seventh Conference on Foundations of Software
Technology and Theoretical Computer Science, Pune, India, Dec. 1987.

[41]
G. Huet.

A Uniform Approach to Type Theory.
Rapport de Recherche INRIA no 795, Février 88.
Course Notes, Institute on Logical Foundations of Functional Programming,
University of Texas at Austin, June 1987.
Final version in

**Logical Foundations of Functional Programming**,
Addison-Wesley, 1989.

[40]
G. Huet.

Extending the Calculus of Constructions with Type:Type.
Unpublished manuscript, 1988.
Available electronically as

pdf.

[39]
G. Huet.

Induction Principles Formalized in the Calculus of Constructions.
in Programming of Future Generation Computers, Ed. K. Fuchi and M. Nivat,
North-Holland, 1988, 205-216.
Available electronically as

pdf.

[38]
G. Huet.

Induction and Recursion in the Theory of Constructions.
Invited paper, Joint Conference on Theory and Practice of Software Development
TAPSOFT’87, Pise, Mars 87.

[37]
G. Huet. Induction, Recursion and Termination in the Theory of Constructions.
Conférence Invitée, Journées Mathématiques et Informatiques, Antibes,
Novembre 86. Revised as (38).

[36]
G. Huet.

Preuves et calculs.
Conférence, Ecole Normale Supérieure, 22 Sept. 1986.

[35]
G. Huet.

Mechanizing Constructive Mathematics.
Invited conference, Conference on Automated Deduction CADE-8,
Oxford, July 1986.

[34]
G. Huet.

Typed Lambda-Calculus and Higher-Order Intuitionistic Logic as Computer
Science Tools.
Invited conference, Association for Symbolic Logic, Indianapolis, April 1986.

[33]
T. Coquand and G. Huet.

The Calculus of Constructions.
Rapport de Recherche Inria no 530, Mai 86.
Final version in Information and Computation 76,2/3, Feb. 88.

[32]
G. Huet.

Formal Structures for Computation and Deduction.
Course Notes, Carnegie-Mellon University, May 1986 (184 pages).
Available as

PDF file.

[31]
Th. Coquand, G. Huet.

Concepts Mathématiques et Informatiques Formalisés
dans le Calcul des Constructions.
Invited paper, European Logic Colloquium, Orsay, July 1985.
Rapport de recherche INRIA 463, Dec. 85.
Published in

**Logic Colloquium 1985**, North-Holland, 1987.

[30]
G. Huet.

Deduction and Computation.
Notes de cours, International Summer
School on Logic of Programming and Calculi of Discrete Design,
Marktoberdorf, Aug. 86.
Published in

Logic of Programming and Calculi of Discrete Design, Ed. M. Broy,
NATO ASI Series, F-36, Springer-Verlag 1987.

[29]
G. Huet.

Deduction and Computation.
Course Notes, Ecole d’Intelligence Artificielle, Vigneu, July 1985.
Published in

**Fundamentals in Artificial Intelligence**,
Eds. W. Bibel and Ph. Jorrand,
Springer-Verlag Lecture Notes in Computer Science vol. 232 (1986) 39-74.
Also Rapport de Recherche Inria no 513, Avril 86.
Final version in next entry.

[28]
G. Huet.

Initiation à la Logique Mathématique.
Notes de Cours, DEA Paris XI, Nov. 1986.

[27]
G. Huet.

Initiation à la Théorie des Catégories.
Notes de Cours, DEA Paris 7, Nov. 1985.
Fac-simile of the original MacWrite document [December 1987 version] available as

PDF document.

[26]
G. Huet.

Cartesian Closed Categories and Lambda-Calculus.
Notes de Cours, Ecole de Printemps d’Informatique Théorique,
Springer-Verlag, LNCS 242 (1986).
Final Version in:

**Logical Foundations of Functional Programming**,
Addison-Wesley, 1989.

[25]
Th. Coquand, G. Huet.

A Selected Bibliography on Constructive Mathematics, Intuitionistic Type
Theory and Higher Order Deduction.
Journal of Symbolic Computation 1 (1985) 323-328.

[24]
G. Huet.

A study of arrow across several mathematical fields: Category Theory,
Intuitionistic Logic, Lambda calculus and Rewriting Reasoning.
Invited
conference, International Conference on rewriting Theory, Dijon, May 1985.

[23]
Th. Coquand, G. Huet.

Constructions: A Higher Order Proof System for
Mechanizing Mathematics.
Invited paper, EUROCAL85, April 1985, Linz, Austria.
Springer Verlag, LNCS 203, pp. 151-184.

[22]
Th. Coquand, G. Huet.

A Theory of Constructions.
Invited conference,
International Symposium on Semantics of Data Types, Sophia-Antipolis, France,
June 1984.

[21]
G. Huet.

The Future of Symbolic Computation: Mathematics versus Languages.
Sigsam Bulletin, Vol 18, No 2, May 1984, pp. 2-5.

[20]
F. Fages, G. Huet.

Complete Sets of Unifiers and Matchers in Equational Theories.
Proceedings, 8th Colloquium on Trees in Algebra and Programming, l’Aquila,
Italia, March 1983. Dans Springer-Verlag LNCS 159 (1983).
Published in Theoretical Computer Science 43 (1986) 189-200.

[19]
V. Donzeau-Gouge, G. Huet, G. Kahn, B. Lang.

Programming Environments based on Structured Editors: The MENTOR
Experience.
In

**Interactive Programming Environments**.
Eds. Barstow D., Shrobe H. and Sandewall E., McGraw Hill, 1984, pp. 128-140.

[18]
G. Huet.

In Defense of Programming Languages Design.
Proceedings, European Conference on Artificial Intelligence,
July 1982, Orsay, France.
Also in

**Progress in Artificial Intelligence**,
Eds. L. Steels and J.A. Campbell, Ellis Horwood 1985.

[17]
G. Huet, J.M. Hullot.

Proofs by Induction in Equational Theories with Constructors.
21st IEEE Symposium on the Foundations of Computer Science, Oct. 1980.
Also JCSS 25,2 (Oct. 82) pp. 239-266.

[16]
G. Huet.

A Complete Proof of Correctness of the Knuth-Bendix Completion
Algorithm.
JCSS 23,1 (Aug. 81) pp. 11-21.

[15]
G. Huet, D. Oppen.

Equations and Rewrite Rules: A Survey.
Computer Science Department Report STAN-CS-80-785, Stanford University,
Jan. 1980.
Also Technical Report CSL-111, SRI International, Jan. 1980.
Also in

**Formal Languages: Perspectives and Open Problems**,
Ed. Book R., Academic Press, 1980, pp. 349-405.

[14]
G. Huet, J.J. Lévy.

Call by Need Computations in Non-Ambiguous Linear Term Rewriting Systems.
Rapport Laboria 359, IRIA, Rocquencourt, France, Aout 1979.

[13]
G. Huet, D. Lankford.

On the Uniform Halting Problem for Term Rewriting Systems.
Rapport Laboria 283, IRIA, Rocquencourt, France, Mars 1978.

[12]
G. Huet.

An Algorithm to Generate the Basis of Solutions to Homogeneous
Linear Diophantine Equations.
Information Processing Letters 7,3 (1978) pp. 144-147.

[11]
G. Huet, B. Lang.

Proving and Applying Program Transformations Expressed with Second
Order Patterns.
Acta Informatica 11 (1978) pp. 31-55.

[10]
G. Huet.

Confluent Reductions: Abstract Properties and Applications to Term
Rewriting Systems.
Proceedings, 18th IEEE Symposium on Foundations of Computer Science,
pp. 30-45.
JACM 27,4, Oct. 1980, pp. 797-821.

[9]
G. Huet.

Résolution d’équations
dans des langages d’ordre 1,2,...,ω.
Thèse de Doctorat es Sciences Mathématiques,
Université Paris VII, Septembre 1976.
Facsimile available electronically as

pdf.

[8]
G. Huet, B. Lang.

Program transformations in classes of interpretations.
Rivista di informatica, vol VV, supplamento al n. 1, gennaio-marzo 1977.

[7]
V. Donzeau-Gouge, G. Huet, G. Kahn, B. Lang.

A structure oriented program editor: a first step towards
computer assisted programming.
International Computing Symposium 1975, North-Holland.
Aussi Rapport de Recherche 114, IRIA-Laboria, Avril 1975.

[6]
G. Huet.

Unification in typed lambda-calculus.
Conference on lambda-calculus and theoretical computer science, Roma,
March 1975.
Springer Verlag LNCS 37, Ed. Bohm C., pp. 192-212.

[5]
G. Huet.

A Unification Algorithm for Typed Lambda-Calculus.
Journal of Theoretical Computer Science, 1,1 1975, pp. 27-58.

[4]
G. Huet.

A Complete Mechanization of Type Theory.
Proceedings, Third International Joint Conference on Artificial Intelligence,
Stanford Aug. 73.
Available as

6Mb PDF file.

[3]
G. Huet.

Constrained Resolution: A Complete Method for Type Theory.
Ph.D. thesis, Computing and Information Sciences, Case Western Reserve
University, Cleveland Ohio.
Report 1117, Jennings Computer Center, Aug. 72.

[2]
G. Huet.

The undecidability of unification in third order logic.
Information and Control 22,3 April 73, pp. 257-267.

[1]
G. Huet.

Experiments with an interactive prover for logic with
equality.
M.S. thesis, Computing and Information Sciences, Case Western Reserve
University, Cleveland Ohio.
Report 1106, Jennings Computer Center, Jan. 71.