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

DOI10.1016/J.JAL.2006.10.001zbMATH Open1138.03014OpenAlexW2138483455WikidataQ58001481 ScholiaQ58001481MaRDI QIDQ2480966FDOQ2480966

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

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

Recommendations

• Higher order unification via explicit substitutions
• scientific article; zbMATH DE number 2208065
• Unification via the \(\lambda s_e\)-style of explicit substitutions
• Higher-order unification with dependent function types
• scientific article; zbMATH DE number 1088023

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)

Cites Work

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

Cited In (7)

• Restricted combinatory unification
• Title not available (Why is that?)
• Higher-order unification revisited: Complete sets of transformations
• Unification via the \(\lambda s_e\)-style of explicit substitutions
• Higher order unification via explicit substitutions
• Unification for $$\lambda $$ -calculi Without Propagation Rules
• A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi

Uses Software

• SUBSEXPL

This page was built for publication: Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions

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