Higher-order unification via combinators

DOI10.1016/0304-3975(93)90075-5zbMath0772.68061OpenAlexW1982776852MaRDI QIDQ2367541

Daniel J. Dougherty

Publication date: 2 September 1993

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(93)90075-5

zbMATH Keywords

program transformationmachine learningautomated theorem provingtyped lambda calculushigher-order unificationtype inference

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Modal logic (including the logic of norms) (03B45)

Related Items

Unification for $$\lambda $$ -calculi Without Propagation Rules ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A combinatory logic approach to higher-order E-unification ⋮ Higher-order matching for program transformation ⋮ Superposition with lambdas ⋮ Restricted combinatory unification ⋮ Higher order unification via explicit substitutions

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The undecidability of the second-order unification problem
• Polymorphic rewriting conserves algebraic strong normalization
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Mechanizing \(\omega\)-order type theory through unification
• Complete sets of transformations for general E-unification
• Higher-order unification revisited: Complete sets of transformations
• An Efficient Unification Algorithm
• A new implementation technique for applicative languages
• Higher-order unification with dependent function types
• Strong reduction and normal form in combinatory logic
• A Short Proof of Curry's Normal Form Theorem
• The Principal Type-Scheme of an Object in Combinatory Logic
• A Complete Mechanization of Second-Order Type Theory
• The undecidability of unification in third order logic