View article

The process of A-lifting (or bracket abstraction) translates expressions in a typed A-calculus into expressions in a typed combinator language. This is of interest because it shows that the A-calculus and the combinator language are equally expressive (as the translation from combinators to X-expressions is rather trivial). This paper studies the similar problems for 2-level A-calculi and 2-level combinator languages. The 2-level nature of the type system enforces a formal distinction between binding times, eg between computations at compile-time and computations at run-time. In this setting the natural formulations of 2-level A-calculi and 2-level combinator languages turn out not to be equally expressive. The translation into 2-level A-calculus is straight-forward but the 2-level A-calculus is too powerful for A-lifting to succeed. We then develop a restriction of the 2-level A-calculus for which A-lifting succeeds and that is as expressive as the 2-level combinator language.