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

DOI10.1016/J.JAL.2006.10.001MaRDI QIDQ2480966zbMATHOpenAlexWikidataFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 1042221 (Why is no real title available?)
• scientific article; zbMATH DE number 1927411 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• scientific article; zbMATH DE number 2208065 (Why is no real title available?)
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Choices in representation and reduction strategies for lambda terms in intensional contexts
• Comparing and implementing calculi of explicit substitutions with eta-reduction
• Explicit substitutions
• Higher order unification via explicit substitutions
• Higher-order unification and matching
• SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The undecidability of the second-order unification problem
• Unification via the \(\lambda s_e\)-style of explicit substitutions

Cited in

(8)

• Unification via the \(\lambda s_e\)-style of explicit substitutions
• A flexible framework for visualisation of computational properties of general explicit substitutions calculi
• scientific article; zbMATH DE number 2208065 (Why is no real title available?)
• Higher order unification via explicit substitutions
• Implementation of higher-order unification based on calculus of explicit substitution
• Unification for \(\lambda\)-calculi without propagation rules
• Restricted combinatory unification
• Higher-order unification revisited: Complete sets of transformations

Describes a project that uses

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)