Observatorio de I+D+i UPM

Descripción
The lambda-calculus is fundamental in computer science. It resists an algebraic treatment because of capture-avoidance side-conditions. Nominal algebra is a logic of equality designed for speci¿cations involving binding. We axiomatise the lambda-calculus using nominal algebra, demonstrate how proofs with these axioms re¿ect the informal arguments on syntax, and we prove the axioms sound and complete. We consider both non-extensional and extensional versions (alpha-beta and alpha-beta-eta equivalence). This connects the nominal approach to names and binding with the view of variables as a syntactic convenience for describing functions. The axiomatisation is ¿nite, close to informal practice, and it ¿ts into a context of other research such as nominal rewriting and nominal sets.
Internacional	Si
JCR del ISI	Si
Título de la revista	JOURNAL OF LOGIC AND COMPUTATION
ISSN	0955-792X
Factor de impacto JCR	0,536
Información de impacto
Volumen
DOI	10.1093/logcom/exp049
Número de revista	0
Desde la página	501
Hasta la página	531
Mes	SEPTIEMBRE
Ranking

Esta actividad pertenece a memorias de investigación

• Autor: Murdoch Gabbay (UPM)

• Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa
• Departamento: Lenguajes y Sistemas Informáticos e Ingeniería de Software