Observatorio de I+D+i UPM

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

Esta actividad pertenece a memorias de investigación

• Autor: Murdoch Gabbay (UPM)

• 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