|
Descripción
|
|
|---|---|
| We consider a term sequent logic for the lambda-calculus. Term sequents are a judgement form similar to the logical judgement form of entailment between sentences, but denoting equality or reducibility between terms. Using term sequents, it is possible to treat lambda-terms almost like logical sentences, and to use proof-theoretic methods to establish their properties. We prove a cut-elimination result for untyped lambda-calculus and describe how this generalises the usual con¿uence result. We give a notion of uniform proof for lambda-terms, and suggest how this can be viewed as a mixed logic-programming/functional programming framework with the ability to assume arbitrary reductions. Finally, we discuss related and future work. | |
|
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
|
246 |
|
DOI
|
|
|
Número de revista
|
0 |
|
Desde la página
|
87 |
|
Hasta la página
|
106 |
|
Mes
|
AGOSTO |
|
Ranking
|
|