Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions

DOI10.1016/j.jal.2006.10.001zbMath1138.03014OpenAlexW2138483455WikidataQ58001481 ScholiaQ58001481MaRDI QIDQ2480966

Flávio L. C. de Moura, Fairouz Kamareddine, Mauricio Ayala-Rincón

Publication date: 7 April 2008

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2006.10.001

zbMATH Keywords

higher-order unificationcalculi of explicit substitutions

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Related Items

Unification for $$\lambda $$ -calculi Without Propagation Rules, A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi, Restricted combinatory unification

Uses Software

• SUBSEXPL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Choices in representation and reduction strategies for lambda terms in intensional contexts
• The undecidability of the second-order unification problem
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Comparing and implementing calculi of explicit substitutions with eta-reduction
• Higher order unification via explicit substitutions
• Unification via the  se-style of explicit substitutions
• SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi ★
• Explicit substitutions