Higher-order unification via combinators

DOI10.1016/0304-3975(93)90075-5MaRDI QIDQ2367541zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 4041327 (Why is no real title available?)
• scientific article; zbMATH DE number 1158760 (Why is no real title available?)
• scientific article; zbMATH DE number 194911 (Why is no real title available?)
• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• scientific article; zbMATH DE number 3280068 (Why is no real title available?)
• scientific article; zbMATH DE number 3423994 (Why is no real title available?)
• A Complete Mechanization of Second-Order Type Theory
• A Short Proof of Curry's Normal Form Theorem
• A new implementation technique for applicative languages
• A unification algorithm for typed -calculus
• An Efficient Unification Algorithm
• Complete sets of transformations for general E-unification
• Higher order E-unification
• Higher-order unification revisited: Complete sets of transformations
• Higher-order unification with dependent function types
• Mechanizing \(\omega\)-order type theory through unification
• Polymorphic rewriting conserves algebraic strong normalization
• Strong reduction and normal form in combinatory logic
• The Principal Type-Scheme of an Object in Combinatory Logic
• The undecidability of the second-order unification problem
• The undecidability of unification in third order logic

Cited in

(21)

• An untyped higher order logic with Y combinator
• Restricted combinatory unification
• Superposition with lambdas
• Higher order E-unification
• scientific article; zbMATH DE number 2208065 (Why is no real title available?)
• The correctness of Newman's typability algorithm and some of its extensions
• Higher-order unification revisited: Complete sets of transformations
• scientific article; zbMATH DE number 7350767 (Why is no real title available?)
• Unification for \(\lambda\)-calculi without propagation rules
• Higher order unification via explicit substitutions
• scientific article; zbMATH DE number 7471678 (Why is no real title available?)
• Higher-order matching for program transformation
• scientific article; zbMATH DE number 7226002 (Why is no real title available?)
• Logic Programming
• scientific article; zbMATH DE number 4068831 (Why is no real title available?)
• 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
• scientific article; zbMATH DE number 3997190 (Why is no real title available?)
• 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)