Descripción
|
|
---|---|
We present a simple but expressive lambda-calculus whose syntax is populated by variables which behave like meta-variables. It can express both capture-avoiding and capturing substitution (instantiation). To do this requires several innovations, including a key insight in the confluence proof and a set of reduction rules which manages the complexity of a calculus of contexts over the ‘vanilla’ lambda-calculus in a very simple and modular way. This calculus remains extremely close in look and feel to a standard lambda-calculus with explicit substitutions, and good properties of the lambda-calculus are preserved. | |
Internacional
|
Si |
JCR del ISI
|
No |
Título de la revista
|
Electronic Notes in Theoretical Computer Science |
ISSN
|
1571-0661 |
Factor de impacto JCR
|
0 |
Información de impacto
|
|
Volumen
|
196 |
DOI
|
10.1016/j.entcs.2007.09.015 |
Número de revista
|
0 |
Desde la página
|
19 |
Hasta la página
|
35 |
Mes
|
ENERO |
Ranking
|