Title :
Higher-order unification via explicit substitutions
Author :
Dowek, Gilles ; Hardin, Thérèse ; Kirchner, Claude
Author_Institution :
Inst. Nat. de Recherche en Inf. et Autom., Le Chesnay, France
Abstract :
Higher-order unification is equational unification for βη-conversion, but it is not first-order equational unification, as substitution has to avoid capture. In this paper higher-order unification is reduced to first-order equational unification in a suitable theory: the λσ-calculus of explicit substitutions
Keywords :
formal logic; lambda calculus; rewriting systems; βη-conversion; capture; equational unification; explicit substitutions; first order rewriting system; first-order equational unification; higher-order unification; lambda calculus; Art; Calculus; Computer languages; Equations; Kernel; Process design;
Conference_Titel :
Logic in Computer Science, 1995. LICS '95. Proceedings., Tenth Annual IEEE Symposium on
Conference_Location :
San Diego, CA
Print_ISBN :
0-8186-7050-9
DOI :
10.1109/LICS.1995.523271
