Toward Introducing Binding-Time Analysis to MetaOCaml
This paper relates 2-level lambda-calculus and
staged lambda-calculus (restricted to 2 stages) to obtain
monovariant binding-time analysis for lambda-calculus that produces
the output in the form of staging annotations.
The relationship between the two lambda-calculi provides us with a
precise and easy instruction on how to implement binding-time analysis
to be incorporated in the staged lambda-calculus.
It forms a basis for introducing binding-time analysis to
full-fledged staged languages such as MetaOCaml.