Observatorio de I+D+i UPM

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

Esta actividad pertenece a memorias de investigación

• Autor: Stéphane Lengrand (Heriot-Watt University, Edinburgh)
• 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