|
Descripción
|
|
|---|---|
| We present a simple 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. These include a Hindley-Milner type system with principal typings and subject reduction, and an applicative characterisation of contextual equivalence. | |
|
Internacional
|
Si |
|
JCR del ISI
|
Si |
|
Título de la revista
|
INFORMATION AND COMPUTATION |
|
ISSN
|
0890-5401 |
|
Factor de impacto JCR
|
0,983 |
|
Información de impacto
|
|
|
Volumen
|
|
|
DOI
|
|
|
Número de revista
|
0 |
|
Desde la página
|
1 |
|
Hasta la página
|
4 |
|
Mes
|
ENERO |
|
Ranking
|
|