Skip to main content
SpringerLink
Log in

Higher Order Unification 30 Years Later

Extended Abstract

  • Conference paper
  • First Online:
Theorem Proving in Higher Order Logics (TPHOLs 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2410))

Included in the following conference series:

Abstract

The talk will present a survey of higher order unification, covering an outline of its historical development, a summary of its applications to three fields: automated theorem proving, and more generally engineering of proof assistants, programming environments and software engineering, and finally computational linguistics. It concludes by a presentation of open problems, and a few prospective remarks on promising future directions. This presentation assumes as background the survey by Gilles Dowek in the Handbook of automated theorem proving [28].

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. G. Amiot. The undecidability of the second order predicate unification problem. Archive for mathematical logic, 30:193–199, 1990.

    Article  MATH  MathSciNet  Google Scholar 

  2. Dale Miller Amy Felty. Specifying theorem provers in a higher-order logic programming language. In Proceedings of the 9th Int. Conference on Automated Deduction (CADE-9), volume 310 of Lecture Notes in Computer Science, pages 61–80. Springer-Verlag, Argonne, Illinois, 1988.

    Chapter  Google Scholar 

  3. Penny Anderson. Represnting proof transformations for program optimization. In Proceedings of the 12th Int. Conference on Automated Deduction (CADE-12), volume 814 of Lecture Notes in Artificial Intelligence, pages 575–589, Nancy, France, 1994. Springer-Verlag.

    Google Scholar 

  4. P.B. Andrews. Resolution in type theory. The Journal of Symbolic Logic, 36(3):414–432, 1971.

    Article  MATH  MathSciNet  Google Scholar 

  5. P.B. Andrews, M. Bishop, S. Issar, D. Nesmith, F. Pfenning, and H. Xi. Tps: a theorem proving system for classical type theory. J. of Automated Reasoning, 16:321–353, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  6. J. Avenhaus and C.A. Loría-Sáenz. Higher-order conditional rewriting and narrowing. In J.-P. Jouannaud, editor, International Conference on Constaints in Computational Logic, volume 845 of Lecture Notes in Computer Science, pages 269–284. Springer-Verlag, 1994.

    Chapter  Google Scholar 

  7. Yves Bekkers, Olivier Ridoux, and Lucien Ungaro. Dynamic memory management for sequential logic programming languages. In IWMM, pages 82–102, 1992.

    Google Scholar 

  8. C. Benzmüller. Extensional higher-order resolution. In Proceedings of the 15th Int. Conference on Automated Deduction (CADE-15), volume 1421 of Lecture Notes in Artificial Intelligence, pages 56–71. Springer-Verlag, Lindau, Germany, 1998.

    Google Scholar 

  9. C. Benzmüller. Equality and extensionality in automated higher-order theorem proving. Doctoral Dissertation, Universität des Saarlandes, Saarbrücken, 1999.

    Google Scholar 

  10. Frédéric Blanqui. Théorie des types et réécriture. Thèse de Doctorat, Université Paris-Sud, 2001.

    Google Scholar 

  11. P. Borovanský. Implementation of higher-order unification based on calculus of explicit substitution. In M. Bartošek, J. Staudek, and J. Wiedermann, editors, SOFSEM: Theory and Practice of Informatics, volume 1012 in Lecture Notes in Computer Science, pages 363–368. Springer-Verlag, 1995.

    Google Scholar 

  12. A. Boudet and E. Contejean. AC-unification of higher-order patterns. In G. Smolka, editor, Principles and Practice of Constraint Programming, volume 1330 of Lecture Notes in Computer Science, pages 267–281. Springer-Verlag, 1997.

    Chapter  Google Scholar 

  13. D. Briaud. Higher order unification as typed narrowing. Technical Report 96-R-112, Centre de recherche en informatique de Nancy, 1996.

    Google Scholar 

  14. Pascal Brisset and Olivier Ridoux. The architecture of an implementation of lambdaprolog: Prolog/mali. Technical Report RR-2392, INRIA, Oct. 1994.

    Google Scholar 

  15. M. Kohlhase, C. Gardent, and K. Konrad. Higher-order colored unification: A linguistic application. J. of Logic, Language and Information, 9:313–338, 2001.

    Google Scholar 

  16. A. Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5(1):56–68, 1940.

    Article  MATH  MathSciNet  Google Scholar 

  17. H. Comon and Y. Jurski. Higher-order matching and tree automata. In M. Nielsen and W. Thomas, editors, Conference on Computer Science Logic, volume 1414 of Lecture Notes in Computer Science, pages 157–176. Springer-Verlag, 1997.

    Chapter  Google Scholar 

  18. D.J. Dougherty. Higher-order unification via combinators. Theoretical Computer Science, 114:273–298, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  19. D.J. Dougherty and P. Johann. A combinatory logic approach to higher-order E-unification. In D. Kapur, editor, Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 79–93. Springer-Verlag, 1992.

    Google Scholar 

  20. G. Dowek. Démonstration automatique dans le calcul des constructions. Thèse de Doctorat, Université de Paris VII, 1991.

    Google Scholar 

  21. G. Dowek. L’indécidabilité du filtrage du troisième ordre dans les calculs avec types dépendants ou constructeurs de types (the undecidability of third order pattern matching in calculi with dependent types or type constructors). Comptes Rendus à l’Académie des Sciences, I, 312(12):951–956, 1991. Erratum, ibid. I, 318, 1994, p. 873.

    MATH  MathSciNet  Google Scholar 

  22. G. Dowek. A second-order pattern matching algorithm in the cube of typed λ-calculi. In A. Tarlecki, editor, Mathematical Foundation of Computer Science, volume 520 of Lecture notes in computer science, pages 151–160. Springer-Verlag, 1991.

    Google Scholar 

  23. G. Dowek. A complete proof synthesis method for the cube of type systems. Journal of Logic and Computation, 3(3):287–315, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  24. G. Dowek. The undecidability of pattern matching in calculi where primitive recursive functions are representable. Theoretical Computer Science, 107:349–356, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  25. G. Dowek. The undecidability of typability in the lambda-pi-calculus. In M. Bezem and J.F. Groote, editors, Typed Lambda Calculi and Applications, volume 664 in Lecture Notes in Computer Science, pages 139–145. Springer-Verlag, 1993.

    Chapter  Google Scholar 

  26. G. Dowek. A unification algorithm for second-order linear terms. Manuscript, 1993.

    Google Scholar 

  27. G. Dowek. Third order matching is decidable. Annals of Pure and Applied Logic, 69:135–155, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  28. G. Dowek. Higher-Order Unification and Matching, chapter 16, pages 1009–1062. Elsevier, 2001.

    Google Scholar 

  29. G. Dowek, T. Hardin, and C. Kirchner. Higher-order unification via explicit substitutions. Information and Computation, 157:183–235, 2000.

    Article  MATH  MathSciNet  Google Scholar 

  30. G. Dowek, T. Hardin, C. Kirchner, and F. Pfenning. Unification via explicit substitutions: the case of higher-order patterns. In M. Maher, editor, Joint International Conference and Symposium on Logic Programming, pages 259–273. The MIT Press, 1996.

    Google Scholar 

  31. C.M. Elliott. Higher-order unification with dependent function types. In N. Dershowitz, editor, Internatinal Conference on Rewriting Techniques and Applications, volume 355 of Lecture Notes in Computer Science, pages 121–136. Springer-Verlag, 1989.

    Google Scholar 

  32. C.M. Elliott. Extensions and applications of higher-order unification. PhD thesis, Carnegie Mellon University, 1990.

    Google Scholar 

  33. W.M. Farmer. A unification algorithm for second-order monadic terms. Annals of Pure and applied Logic, 39:131–174, 1988.

    Article  MATH  MathSciNet  Google Scholar 

  34. W.M. Farmer. Simple second order languages for which unification is undecidable. Theoretical Computer Science, 87:25–41, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  35. Amy Felty. Implementing tactics and tacticals in a higher-order logic programming language. Journal of Automated Reasoning, 11:43–81, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  36. C. Gardent. Deaccenting and higher-order unification. J. of Logic, Language and Information, 9:313–338, 2000.

    Article  MATH  Google Scholar 

  37. C. Gardent and M. Kohlhase. Focus and higher-order unification. In 16th International Conference on Computational Linguistics, Copenhagen, 1996.

    Google Scholar 

  38. C. Gardent and M. Kohlhase. Higher-order coloured unification and natural language semantics. In ACL, editor, 34th Annual Meeting of the Association for Computational Linguistics, Santa Cruz, 1996.

    Google Scholar 

  39. W.D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225–230, 1981.

    Article  MATH  MathSciNet  Google Scholar 

  40. J. Goubault. Higher-order rigid E-unification. In F. Pfenning, editor, 5th International Conference on Logic Programming and Automated Reasoning, volume 822 in Lecture Notes in Artificial Intelligence, pages 129–143. Springer-Verlag, 1994.

    Google Scholar 

  41. W.E. Gould. A matching procedure for ω-order logic. Scientific report 4, AFCRL 66-781 (contract AF 19 (628)-3250) AD 646 560.

    Google Scholar 

  42. J.R. Guard. Automated logic for semi-automated mathematics. Scientific report 1, AFCRL 64-411 (contract AF 19 (628)-3250) AS 602 710, 1964.

    Google Scholar 

  43. M. Hagiya. Programming by example and proving by example using higher-order unification. In M.E. Stickel, editor, Conference on Automated Deduction, volume 449 in Lecture Notes in Computer Science, pages 588–602. Springer-Verlag, 1990.

    Google Scholar 

  44. M. Hagiya. Higher-order unification as a theorem proving procedure. In K. Furukawa, editor, International Conference on Logic Programming, pages 270–284. MIT Press, 1991.

    Google Scholar 

  45. John Hannan and Dale Miller. Uses of higher-order unification for implementing programs transformers. In R.A. Kowalski an K.A. Bowen, editor, International Conference and Symposium on Logic Programming, pages 942–959, 1988.

    Google Scholar 

  46. G. Huet. The undecidability of unification in third order logic. Information and Control, 22:257–267, 1973.

    Article  MathSciNet  MATH  Google Scholar 

  47. G. Huet. Résolution d’équations dans les langages d’ordre 1,2,..., ω. Thèse d’État, Université de Paris VII, 1976.

    Google Scholar 

  48. G. Huet and B. Lang. Proving and applying program transformations expressed with second order patterns. Acta Informatica, 11:31–55, 1978.

    Article  MATH  MathSciNet  Google Scholar 

  49. GĂ©rard Huet. Constrained resolution: A complete method for higher order logic. PhD thesis, Case Western University, Aug. 1972.

    Google Scholar 

  50. D.C. Jensen and T. Pietrzykowski. Mechanizing ω-order type theory through unification. Theoretical Computer Science, 3:123–171, 1976.

    Article  MathSciNet  Google Scholar 

  51. Frank Pfenning, Joëlle Despeyroux, and Carsten Schürmann. Primitive recursion for higher-order syntax. In R. Hindley, editor, Proceedings of the 3rd Int. Conference on Typed Lambda Calculus and Applications (TLCA’ 97), volume 1210 of Lecture Notes in Computer Science, pages 147–163, Nancy, France, 1997. Springer-Verlag.

    Google Scholar 

  52. Patricia Johann and Michael Kohlhase. Unification in an extensional lambda calculus with ordered function sorts and constant overloading. In Alan Bundy, editor, Conference on Automated Deduction, volume 814 in Lecture Notes in Artificial Intelligence, pages 620–634. Springer-Verlag, 1994.

    Google Scholar 

  53. C. Kirchner and Ch. Ringeissen. Higher-order equational unification via explicit substitutions. In M. Hanus, J. Heering, and K. Meinke, editors, Algebraic and Logic Programming, International Joint Conference ALP’97-HOA’97, volume 1298 of Lecture Notes in Computer Science, pages 61–75. Springer-Verlag, 1997.

    Chapter  Google Scholar 

  54. K. Kwon and G. Nadathur. An instruction set for higher-order hereditary harrop formulas (extended abstract). In Proceedings of the Workshop on the lambda Prolog Programming Language, UPenn Technical Report MS-CIS-92-86, 1992.

    Google Scholar 

  55. Peter Lee, Frank Pfenning, John Reynolds, Gene Rollins, and Dana Scott. Research on semantically based program-design environments: The ergo project in 1988. Technical Report CMU-CS-88-118, Computer Science Department, Carnegie Mellon University, 1988.

    Google Scholar 

  56. J. Levy. Linear second order unification. In H. Ganzinger, editor, Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 332–346. Springer-Verlag, 1996.

    Google Scholar 

  57. Jordi Levy and Margus Veanes. On unification problems in restricted second-order languages. In Annual Conf. of the European Ass. of Computer Science Logic (CSL98), Brno, Czech Republic, 1998.

    Google Scholar 

  58. Jordi Levy and Mateu Villaret. Linear second-order unification and context unification with tree-regular constraints. In Proceedings of the 11th Int. Conf. on Rewriting Techniques and Applications (RTA 2000), volume 1833 of Lecture Notes in Computer Science, pages 156–171, Norwich, UK, 2000. Springer-Verlag.

    Chapter  Google Scholar 

  59. R. Loader. The undecidability of λ-definability. To appear in Church memorial volume, 1994.

    Google Scholar 

  60. R. Loader. Higher order β matching is undecidable. Private communication, 2001.

    Google Scholar 

  61. C.L. Lucchesi. The undecidability of the unification problem for third order languages. Technical Report CSRR 2060, Department of applied analysis and computer science, University of Waterloo, 1972.

    Google Scholar 

  62. Stuart M. Shieber Mary Dalrymple and Fernando C.N. Pereira. Ellipsis and higher-order unification. Linguistic and Philosophy, 14:399–452, 1991.

    Article  Google Scholar 

  63. R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192:3–29, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  64. Raymond McDowell and Dale Miller. Reasoning with higher-order abstract syntax in a logical framework. ACM Transactions on Computational Logic (TOCL), 3:80–136, 2002.

    Article  MathSciNet  Google Scholar 

  65. Dale Miller. Abstractions in logic programming. In P. Odifreddi, editor, Logic and computer science, pages 329–359. Academic Press, 1991.

    Google Scholar 

  66. Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14:321–358, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  67. Dale Miller and Gopalan Nadathur. A logic programming approach to manipulating formulas and programs. In IEEE Symposium on Logic Programming, pages 247–255, San Francisco, California, 1986.

    Google Scholar 

  68. Dale Miller and Gopalan Nadathur. Some uses of higher-order logic in computational linguistics. In 24th Annual Meeting of the Association for Computational Linguistics, pages 247–255, 1986.

    Google Scholar 

  69. O. Müller and F. Weber. Theory and practice of minimal modular higher-order E-unification. In A. Bundy, editor, Conference on Automated Deduction, volume 814 in Lecture Notes in Artificial Intelligence, pages 650–664. Springer-Verlag, 1994.

    Google Scholar 

  70. Gopalan Nadathur. An explicit substitution notation in a λprolog implementation. In First International Workshop on Explicit Substitutions, 1998.

    Google Scholar 

  71. Gopalan Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD thesis, University of Pennsylvania, Dec. 1986.

    Google Scholar 

  72. Gopalan Nadathur and Dale Miller. Higher-order horn clauses. J. of the Association for Computing Machinery, 37:777–814, 1990.

    MATH  MathSciNet  Google Scholar 

  73. Gopalan Nadathur and Dale Miller. Higher-order logic programming. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of logic in artificial intelligence and logic programming, volume 5, pages 499–590. Clarendon Press, 1998.

    Google Scholar 

  74. Gopalan Nadathur and D.J. Mitchell. System description: A compiler and abstract machine based implementation of λprolog. In Conference on Automated Deduction, 1999.

    Google Scholar 

  75. T. Nipkow. Higher-order critical pairs. In Logic in Computer Science, pages 342–349, 1991.

    Google Scholar 

  76. T. Nipkow. Higher-order rewrite systems. In Proceedings of the 6th Int. Conf. on Rewriting Techniques and Applications (RTA-95), volume 914 of Lecture Notes in Computer Science, pages 256–256, Keiserlautern, Germany, 1995. Springer-Verlag.

    Google Scholar 

  77. T. Nipkow and Ch. Prehofer. Higher-order rewriting and equational reasoning. In W. Bibel and P.H. Schmitt, editors, Automated Deduction-A Basis for Applications, volume 1, pages 399–430. Kluwer, 1998.

    Google Scholar 

  78. Tobias Nipkow and Zhenyu Qian. Modular higher-order e-unification. In Proceedings of the 4th Int. Conf. on Rewriting Techniques and Applications (RTA), volume 488 of Lecture Notes in Computer Science, pages 200–214. Springer-Verlag, 1991.

    Google Scholar 

  79. Tobias Nipkow and Zhenyu Qian. Reduction and unification in lambda calculi with a general notion of subtype. Journal of Automated Reasoning, 12:389–406, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  80. V. Padovani. Fourth-order matching is decidable. Manuscript, 1994.

    Google Scholar 

  81. V. Padovani. Decidability of all minimal models. In S. Berardi and M. Coppo, editors, Types for Proof and Programs 1995, volume 1158 in Lecture Notes in Computer Science, pages 201–215. Springer-Verlag, 1996.

    Google Scholar 

  82. V. Padovani. Filtrage d’ordre supérieur. Thèse de Doctorat, Université de Paris VII, 1996.

    Google Scholar 

  83. Larry C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and computer science, pages 361–385. Academic Press, 1991.

    Google Scholar 

  84. F. Pfenning. Partial polymorphic type inference and higher-order unification. In Conference on Lisp and Functional Programming, pages 153–163, 1988.

    Google Scholar 

  85. F. Pfenning. Logic programming in the LF logical framework. In G. Huet and G. Plotkin, editors, Logical frameworks, pages 149–181. Cambridge University Press, 1991.

    Google Scholar 

  86. F. Pfenning. Unification and anti-unification in the calculus of constructions. In Logic in Computer Science, pages 74–85, 1991.

    Google Scholar 

  87. F. Pfenning and I. Cervesato. Linear higher-order pre-unification. In Logic in Computer Science, 1997.

    Google Scholar 

  88. Frank Pfenning and Carsten Schürmann. System description: Twelf — A metalogical framework for deductive systems. In Proceedings of the 16th Int. Conference on Automated Deduction (CADE-16), volume 1632 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1999.

    Google Scholar 

  89. T. Pietrzykowski. A complete mecanization of second-order type theory. J. of the Association for Computing Machinery, 20:333–364, 1973.

    MATH  MathSciNet  Google Scholar 

  90. G. Plotkin. Building-in equational theories. Machine Intelligence, 7:73–90, 1972.

    MathSciNet  MATH  Google Scholar 

  91. C. Prehofer. Decidable higher-order unification problems. In A. Bundy, editor, Conference on Automated Deduction, volume 814 of Lecture Notes in Artificial Intelligence, pages 635–649. Springer-Verlag, 1994.

    Google Scholar 

  92. C. Prehofer. Higher-order narrowing. In Logic in Computer Science (LICS’94, pages 507–516, 1994.

    Google Scholar 

  93. C. Prehofer. Solving higher-order equations: From logic to programming. Doctoral thesis, Technische Universität München. Technical Report TUM-19508, Institut für Informatik, TUM, München, 1995.

    Google Scholar 

  94. C. Prehofer. Solving Higher-Order Equations: From Logic to Programming. Progress in theoretical coputer science. Birkhäuser, 1998.

    Google Scholar 

  95. S. Pulman. Higher-order unification and the interpretation of focus. Linguistics and Philosophy, 20:73–115, 1997.

    Article  Google Scholar 

  96. D. Pym. Proof, search, and computation in general logic. Doctoral thesis, University of Edinburgh, 1990.

    Google Scholar 

  97. Z. Qian. Higher-order equational logic programming. In Principle of Programming Languages, pages 254–267, 1994.

    Google Scholar 

  98. Z. Qian and K. Wang. Higher-order equational E-unification for arbitrary theories. In K. Apt, editor, Joint International Conference and Symposium on Logic Programming, 1992.

    Google Scholar 

  99. Z. Qian and K. Wang. Modular AC unification of higher-order patterns. In J.-P. Jouannaud, editor, International Conference on Constaints in Computational Logic, volume 845 of Lecture Notes in Computer Science, pages 105–120. Springer-Verlag, 1994.

    Chapter  Google Scholar 

  100. J.A. Robinson. New directions in mechanical theorem proving. In A.J.H. Morrell, editor, International Federation for Information Processing Congress, 1968, pages 63–67. North Holland, 1969.

    Google Scholar 

  101. J.A. Robinson. A note on mechanizing higher order logic. Machine Intelligence, 5:123–133, 1970.

    Google Scholar 

  102. H. Saïdi. Résolution d’équations dans le système T de Gödel. Mémoire de DEA, Université de Paris VII, 1994.

    Google Scholar 

  103. M. Schmidt-Schauß. Unification of stratified second-order terms. Technical Report 12, J.W.Goethe-Universität, Frankfurt, 1994.

    Google Scholar 

  104. M. Schmidt-Schauß. Decidability of bounded second order unification. Technical Report 11, J.W.Goethe-Universität, Frankfurt, 1999.

    Google Scholar 

  105. M. Schmidt-Schauß and K.U. Schulz. Solvability of context equations with two context variables is decidable. In H. Ganzinger, editor, Conference on Automated Deduction, volume 1632 in Lecture Notes in Artificial Intelligence, pages 67–81, 1999.

    Google Scholar 

  106. A. Schubert. Linear interpolation for the higher order matching problem. In M. Bidoit and M. Dauchet, editors, Theory and Practice of Software Development, volume 1214 of Lecture Notes in Computer science, pages 441–452. Springer-Verlag, 1997.

    Chapter  Google Scholar 

  107. A. Schubert. Second-order unification and type inference for Church-style polymorphism. In Principle of Programming Languages, pages 279–288, 1998.

    Google Scholar 

  108. W. Snyder. Higher-order E-unification. In M. E. Stickel, editor, Conference on Automated Deduction, volume 449 of Lecture Notes in Artificial Intelligence, pages 573–587. Springer-Verlag, 1990.

    Google Scholar 

  109. W. Snyder and J. Gallier. Higher order unification revisited: Complete sets of tranformations. Journal of Symbolic Computation, 8(1 & 2):101–140, 1989. Special issue on unification. Part two.

    Article  MathSciNet  MATH  Google Scholar 

  110. W. Snyder and J. Gallier. Higher-order unification revisited: Complete sets of transformations. Journal of Symbolic Computation, 8:101–140, 1989.

    Article  MathSciNet  MATH  Google Scholar 

  111. J. Springintveld. Algorithms for type theory. Doctoral thesis, Utrecht University, 1995.

    Google Scholar 

  112. J. Springintveld. Third-order matching in presence of type constructors. In M. Dezani-Ciancagliani and G. Plotkin, editors, Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, pages 428–442. Springer-Verlag, 1995.

    Chapter  Google Scholar 

  113. J. Springintveld. Third-order matching in the polymorphic lambda calculus. In G. Dowek, J. Heering, K. Meinke, and B. Mßoller, editors, Higher-order Algebra, Logic and Term Rewriting, volume 1074 of Lecture Notes in Computer Science, pages 221–237. Springer-Verlag, 1995.

    Google Scholar 

  114. Fernando C.N. Pereira Stuart, M. Shieber, and Mary Dalrymple. Interactions of scope and ellipsis. Linguistics and Philosophy, 19:527–552, 1996.

    Article  Google Scholar 

  115. D.A. Wolfram. The clausal theory of types. Doctoral thesis, University of Cambridge, 1989.

    Google Scholar 

  116. M. Zaionc. The regular expression description of unifier set in the typed λ-calculus. Fundementa Informaticae, X:309–322, 1987.

    MathSciNet  Google Scholar 

  117. M. Zaionc. Mechanical procedure for proof construction via closed terms in typed λ-calculus. Journal of Automated Reasoning, 4:173–190, 1988.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA-Rocquencourt, BP 105, F-78153, Le Chesnay Cedex

    GĂ©rard Huet

Authors
  1. GĂ©rard Huet
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. NASA Langley Research Center, MS 130, Hampton, VA, 23681, USA

    Victor A. Carreño

  2. ICASE-Langley Research Center, MS 132C, Hampton, VA, 23681, USA

    César A. Muñoz

  3. Electrical and Computer Engineering, Concordia University, 1455 de Maisonneuve Blvd.W., Montréal, Québec, H3G 1M8, Canada

    Sofiène Tahar

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Huet, G. (2002). Higher Order Unification 30 Years Later. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2002. Lecture Notes in Computer Science, vol 2410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45685-6_2

Download citation

  • DOI: https://doi.org/10.1007/3-540-45685-6_2

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44039-0

  • Online ISBN: 978-3-540-45685-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation