• DocumentCode
    3295946
  • 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
  • fYear
    1995
  • fDate
    26-29 Jun 1995
  • Firstpage
    366
  • Lastpage
    374
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1995. LICS '95. Proceedings., Tenth Annual IEEE Symposium on
  • Conference_Location
    San Diego, CA
  • ISSN
    1043-6871
  • Print_ISBN
    0-8186-7050-9
  • Type

    conf

  • DOI
    10.1109/LICS.1995.523271
  • Filename
    523271
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3295946