In order to enable a compiler to emit fast code, the authors annotate source programs with propositions during a program analysis phase. These propositions later justify certain transformations. While this is a manageable task in the analysis of classical programs, it becomes complex for higher-order programs.

The so-called lightweight closure conversion deserves attention in the field of lexically scoped functional languages. A closure is meant to be a data structure that contains pure code (closed &lgr;-abstraction) and the values of the free variables of the original procedure, the so-called  environment. 

In many cases, a closure need not include all of the free variables of a procedure, because some of the free variables are available at all of the places where the closure might be invoked. These variables are called dynamic because they behave the same as they would if the language used dynamic scope. The incomplete closure is then called a “lightweight” closure. Several examples shed light on the possible introduction of lightweight closures and where they must be prohibited.

In the rest of the paper, the simple language λ _{i n} is presented. It consists of an untyped &lgr;-calculus with integer constants, Boolean constants, conditionals, and primitive operators. It follows the syntax and semantics of the annotations, which are added to the program during the analysis. These annotations may be derived as the solution to a deductive system, for which soundness is proven.

The paper aims at a theoretically oriented audience, in that many proofs and formalisms are included in the well-founded but very technical text.