scientific article; zbMATH DE number 2208065

MaRDI QIDQ5693576zbMATH OpenFDO

Authors Mauricio Ayala-Rincón, Fairouz Kamareddine

Publication date 26 September 2005

zbMATH Keywords

higher-order unificationexplicit substitutionsterms\(\lambda\sigma\)-calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Recommendations

• Unification via the \(\lambda s_e\)-style of explicit substitutions
• Higher-order unification via combinators
• Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions
• Higher order unification via explicit substitutions
• scientific article; zbMATH DE number 1088023

Cited in

(6)

• Unification via the \(\lambda s_e\)-style of explicit substitutions
• Unification for \(\lambda\)-calculi without propagation rules
• Higher order unification via explicit substitutions
• General \(E\)-unification with eager variable elimination and a nice cycle rule
• Comparing and implementing calculi of explicit substitutions with eta-reduction
• Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions

This page was built for publication:

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