Stackability in the simply-typed call-by-value lambda calculus

This paper addresses two issues: 1. (1) What it means for a higher-order, eager functional language to be implemented with a single, global, stack-based environment and 2. (2) how the existence of such an environment can be predicted statically. The central theme is the use of the λ-abstraction to control the extent or lifetime of bindings. All programs in a higher-order, call-by-name language can be implemented with a stack environment. The reason: soundness of η-expansion and decurrying for call-by-name. However, η-expansion is unsound for call-by-value. Hence, we must identify a subset of the simply typed, call-by-value λ-calculus, where the λ-abstraction can serve as the block construct for a stack implementation. The essence of environment stackability is that the shape of the environment remains the same before and after the execution of an expression. Thus, if a closure is returned as a value, the environment trapped in it must be a subenvironment of the global environment. This yields a dynamic criterion for stackability — indeed, it is the downwards funargs criterion of the LISP community. A safe static criterion can now be found via closure analysis.