Higher Order Unification 30 Years Later

This publication has 72 references indexed in Scilit:

• The undecidability of typability in the Lambda-Pi-calculus
  Published by Springer Nature ,2006
• Specifying theorem provers in a higher-order logic programming language
  Published by Springer Nature ,2005
• Reasoning with higher-order abstract syntax in a logical framework
  ACM Transactions on Computational Logic, 2002
• Higher-order rewrite systems and their confluence
  Theoretical Computer Science, 1998
• Extensional higher-order resolution
  Published by Springer Nature ,1998
• Simple second-order languages for which unification is undecidable
  Theoretical Computer Science, 1991
• The undecidability of the second-order unification problem
  Theoretical Computer Science, 1981
• Mechanizing ω-order type theory through unification
  Theoretical Computer Science, 1976
• A Complete Mechanization of Second-Order Type Theory
  Journal of the ACM, 1973
• Resolution in type theory
  The Journal of Symbolic Logic, 1971