Abstract



Twolevel lambdacalculus is designed to provide a mathematical model of capturing substitution, also called instantiation. Instantiation is a feature of the `informal metalevel¿; it appears pervasively in specifications of the syntax and semantics of formal languages. The twolevel lambdacalculus has two levels of variable. Lambdaabstraction and betareduction exist for both levels. A level 2 betareduct, triggering a substitution of a term for a level 2 variable, does not avoid capture for level 1 abstractions. This models metavariables and instantiation as appears at the informal metalevel. In this paper we lay down the syntax of the twolevel lambdacalculus; we develop theories of freshness, alphaequivalence, and betareduction; 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 longerterm goals of developing a foundation for theoremprovers 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

15710661 
Impact factor JCR

0 
Impact info


Volume

246 


Journal number

0 
From page

107 
To page

129 
Month

AGOSTO 
Ranking
