Observatorio de I+D+i UPM

Descripción
Two-level lambda-calculus is designed to provide a mathematical model of capturing substitution, also called instantiation. Instantiation is a feature of the `informal meta-level¿; it appears pervasively in specifications of the syntax and semantics of formal languages. The two-level lambda-calculus has two levels of variable. Lambda-abstraction and beta-reduction exist for both levels. A level 2 beta-reduct, triggering a substitution of a term for a level 2 variable, does not avoid capture for level 1 abstractions. This models meta-variables and instantiation as appears at the informal meta-level. In this paper we lay down the syntax of the two-level lambda-calculus; we develop theories of freshness, alpha-equivalence, and beta-reduction; and we prove confluence. In doing this we give nominal terms unknowns ¿ which are level 2 variables and appear in several previous papers ¿ a functional meaning. In doing this we take a step towards longer-term goals of developing a foundation for theorem-provers which directly support reasoning in the style of nominal rewriting and nominal algebra, and towards a mathematics of functions which can bind names in their arguments.
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	107
Hasta la página	129
Mes	AGOSTO
Ranking

Esta actividad pertenece a memorias de investigación

• Autor: Dominic P. Mulligan (Heriot-Watt University, Edinburgh, UK)
• 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