Observatorio de I+D+i UPM

Descripción
We present the Lambda Context Calculus. This simple lambda-calculus features variables arranged in a hierarchy of strengths such that substitution of a strong variable does not avoid capture with respect to abstraction by a weaker variable. This allows the calculus to express both capture-avoiding and capturing substitution (instantiation). The reduction rules extend the `vanilla¿ lambda-calculus in a simple and modular way and preserve the look and feel of a standard lambda-calculus with explicit substitutions. Good properties of the lambda-calculus are preserved. The LamCC is con¿uent, and a natural injection into the LamCC of the untyped lambda-calculus exists and preserves strong normalisation. We discuss the calculus and its design with full proofs. In the presence of the hierarchy of variables, functional binding splits into a functional abstraction ¿ (lambda) and a name- binder b (new). We investigate how the components of this calculus interact with each other and with the reduction rules, with examples. In two more extended case studies we demonstrate how global state can be expressed, and how contexts and contextual equivalence can be naturally internalised using function application.
Internacional	Si
JCR del ISI	Si
Título de la revista	INFORMATION AND COMPUTATION
ISSN	0890-5401
Factor de impacto JCR	1,504
Información de impacto
Volumen	207
DOI	10.1016/j.ic.2009.06.004
Número de revista	12
Desde la página	1369
Hasta la página	1400
Mes	DICIEMBRE
Ranking

Esta actividad pertenece a memorias de investigación

• Autor: Stéphane Lengrand (CNRS and École Polytechnique, Paris, France)
• 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