Observatorio de I+D+i UPM

Memorias de investigación
Research Publications in journals:
A nominal axiomatisation of the lambda-calculus
Year:2009
Research Areas
  • Programming language
Information
Abstract
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.
International
Si
JCR
Si
Title
JOURNAL OF LOGIC AND COMPUTATION
ISBN
0955-792X
Impact factor JCR
0,536
Impact info
Volume
10.1093/logcom/exp049
Journal number
0
From page
501
To page
531
Month
SEPTIEMBRE
Ranking
Participants
  • Autor: Murdoch Gabbay (UPM)
Research Group, Departaments and Institutes related
  • 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
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)