Matching and alpha-equivalence check for nominal terms

TY - JOUR

T1 - Matching and alpha-equivalence check for nominal terms

AU - Calves, Christophe

AU - Fernandez, Maribel

PY - 2010/8

Y1 - 2010/8

N2 - Nominal terms generalise first-order terms by including abstraction and name swapping constructs, alpha-equivalence can be easily axiomatised using name swappings and a freshness relation, which makes the nominal approach well adapted to the specification of systems that involve binders. Nominal matching is matching modulo alpha-equivalence and has applications in programming languages, rewriting, and theorem proving. In this paper, we describe efficient algorithms to check the validity of equations involving binders and to solve matching problems modulo alpha-equivalence, using the nominal approach. (C) 2009 Elsevier Inc. All rights reserved.

AB - Nominal terms generalise first-order terms by including abstraction and name swapping constructs, alpha-equivalence can be easily axiomatised using name swappings and a freshness relation, which makes the nominal approach well adapted to the specification of systems that involve binders. Nominal matching is matching modulo alpha-equivalence and has applications in programming languages, rewriting, and theorem proving. In this paper, we describe efficient algorithms to check the validity of equations involving binders and to solve matching problems modulo alpha-equivalence, using the nominal approach. (C) 2009 Elsevier Inc. All rights reserved.

U2 - 10.1016/j.jcss.2009.10.003

DO - 10.1016/j.jcss.2009.10.003

M3 - Article

VL - 76

SP - 283

EP - 301

JO - JOURNAL OF COMPUTER AND SYSTEM SCIENCES

JF - JOURNAL OF COMPUTER AND SYSTEM SCIENCES

IS - 5

ER -