Observatorio de I+D+i UPM

Memorias de investigación
Research Publications in journals:
Nominal Rewriting (journal version)
Year:2007
Research Areas
  • Programming language
Information
Abstract
Nominal rewriting is based on the observation that if we add support for α-equivalence to first-order syntax using the nominal-set approach, then systems with binding, including higher-order reduction schemes such as λ-calculus beta-reduction, can be smoothly represented. Nominal rewriting maintains a strict distinction between variables of the object-language (atoms) and of the meta-language (variables or unknowns). Atoms may be bound by a special abstraction operation, but variables cannot be bound, giving the framework a pronounced first-order character, since substitution of terms for variables is not capture-avoiding. We show how good properties of first-order rewriting survive the extension, by giving an efficient rewriting algorithm, a critical pair lemma, and a confluence theorem for orthogonal systems.
International
Si
JCR
Si
Title
INFORM COMPUT
ISBN
0890-5401
Impact factor JCR
0,983
Impact info
Volume
205
Journal number
6
From page
917
To page
965
Month
SIN MES
Ranking
Participants
  • Autor: Maribel Fernández (King¿s College London)
  • Autor: Murdoch Gabbay (UPM)
Research Group, Departaments and Institutes related
  • Creador: No seleccionado
S2i 2020 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)