Memorias de investigación
Research Publications in journals:
Two-level lambda-calculus
Year:2009

Research Areas
  • Programming language

Information
Abstract
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.
International
Si
JCR
No
Title
Electronic Notes in Theoretical Computer Science
ISBN
1571-0661
Impact factor JCR
0
Impact info
Volume
246
Journal number
0
From page
107
To page
129
Month
AGOSTO
Ranking
Participants
  • Autor: Dominic P. Mulligan Heriot-Watt University, Edinburgh, UK
  • Autor: Murdoch Gabbay . UPM

Research Group, Departaments and Institutes related
  • 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