Higher-order unification via combinators

DOI10.1016/0304-3975(93)90075-5zbMATH Open0772.68061OpenAlexW1982776852MaRDI QIDQ2367541FDOQ2367541

Authors: 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

Recommendations

• A combinatory logic approach to higher-order E-unification
• Higher order unification via explicit substitutions
• Decidable higher-order unification problems
• Modular higher-order E-unification
• Higher-order unification, polymorphism, and subsorts
• A higher-order unification algorithm for inductive types and dependent types
• scientific article; zbMATH DE number 1324447
• Restricted combinatory unification
• Mechanizing Mathematical Reasoning
• Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type

zbMATH Keywords

machine learningautomated theorem provingtyped lambda calculusprogram transformationtype inferencehigher-order unification

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• An Efficient Unification Algorithm
• The Principal Type-Scheme of an Object in Combinatory Logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• A new implementation technique for applicative languages
• Title not available (Why is that?)
• Title not available (Why is that?)
• A unification algorithm for typed \(\overline\lambda\)-calculus
• The undecidability of the second-order unification problem
• Polymorphic rewriting conserves algebraic strong normalization
• Complete sets of transformations for general E-unification
• Higher-order unification revisited: Complete sets of transformations
• Title not available (Why is that?)
• 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 undecidability of unification in third order logic
• A Complete Mechanization of Second-Order Type Theory
• Mechanizing \(\omega\)-order type theory through unification
• Higher order E-unification

Cited In (21)

• Restricted combinatory unification
• Superposition with lambdas
• Higher order E-unification
• Title not available (Why is that?)
• The correctness of Newman's typability algorithm and some of its extensions
• Title not available (Why is that?)
• Higher-order unification revisited: Complete sets of transformations
• Unification for \(\lambda\)-calculi without propagation rules
• Higher order unification via explicit substitutions
• Title not available (Why is that?)
• Higher-order matching for program transformation
• Title not available (Why is that?)
• Logic Programming
• Title not available (Why is that?)
• Unification under a mixed prefix
• Higher-order unification with dependent function types
• Modular higher-order E-unification
• Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type
• Title not available (Why is that?)
• An untyped higher order logic with Y combinator
• A combinatory logic approach to higher-order E-unification

This page was built for publication: Higher-order unification via combinators

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2367541)