|
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
|
|