Unification via the se-style of explicit substitutions
From MaRDI portal
Publication:2743636
DOI10.1093/jigpal/9.4.489zbMath0987.03012OpenAlexW2040894779MaRDI QIDQ2743636
Fairouz Kamareddine, Mauricio Ayala-Rincón
Publication date: 19 June 2002
Published in: Logic Journal of IGPL (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1093/jigpal/9.4.489
Functional programming and lambda calculus (68N18) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)
Related Items (7)
Unification for $$\lambda $$ -calculi Without Propagation Rules ⋮ Nominal essential intersection types ⋮ Completeness in PVS of a nominal unification algorithm ⋮ Comparing Calculi of Explicit Substitutions with Eta-reduction ⋮ Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions ⋮ Comparing and implementing calculi of explicit substitutions with eta-reduction ⋮ SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi ★
This page was built for publication: Unification via the se-style of explicit substitutions