Publications of G. Huet

Publications of Gérard Huet

[122] Sriram Krishnan, Amba Kulkarni and Gérard Huet. Normalized Dataset for Sanskrit Word Segmentation and Morphological Parsing. Language Resources and Evaluation, August 2024. Available at Springer Link.

[121] Gérard Huet. Hoisting the colors of Sanskrit. Proceedings of the Seventh International Symposium on Sanskrit Computational Linguistics, Pondicherry, February 2024. Available at ACL Anthology.

[120] Gérard Huet. Canonical Basis of Commuting Diagrams. Application to the Mechanical Synthesis of Coherence Conditions. In "A Century since Principia's Substitution Bedazzled Haskell Curry - in honor of Jonathan Seldin's 80th Anniversary", ed. Fairouz Kamareddine, College Publications 2023. [This paper was presented at a category theory meeting in Boulder in 1987, and until now unpublished. These results appeared first in the Category Theory course notes referenced in [27], which are also reproduced in this volume].

[119] Sriram Krishnan, Amba Kulkarni and Gérard Huet. Validation and Normalization of DCS corpus and Development of the Sanskrit {Heritage} Engine’s Segmenter. 18th World Sanskrit Conference, Canberra, 2023. Published in ACL Anthology.

[118] Gérard Huet. Design of a Sanskrit Reader Assistant. Sanskrit in China International Conference, Chengdu, 2019. To appear, Acta Orientalia LXXX, ed. Claus Peter Zoller, 2021. Available electronically as Word document.

[117] Gérard Huet. Sanskrit lexicography, past and future. in Research on the Language and Script in Buddhist Sutras, ed. Pr Li Wei. Hangzhou Buddhist Academy, 2019. Available electronically as Pdf document.

[116] Gérard Huet. Comprendre le Sanskrit : de la Grammaire de {Pāṇini} aux Machines d'{Eilenberg}. In "Langue et science, langage et pensée", ed. Jean-Noël Robert; ed. Odile Jacob, 2020. Available electronically as Word document.

[115] Gérard Huet and Amba Kulkarni, eds. Computational Sanskrit and Digital Humanities. DK Publishers, Delhi, 2018. Digital edition available as pdf document.

[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 [109]. 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. This presents the Gilbreath trick Coq axiomatisation, which was demonstrated at the workshop on Logical Frameworks in Edinburgh in May 1991. It came from a card trick played by Nicolaas de Bruijn to my daughter Isabelle. Daniel de Rauglaudre provided a graphic postcript animation for the card shuffle demonstration. The conference paper is basically a shortening of the full note referenced below as [50], and available as pdf.

[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. Available electronically as pdf.

[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: 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. Available electronically as pdf.

[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. Available electronically as pdf.

[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. Available as 1.6Mb PDF file.

[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.