A Unified Framework for Binding-Time Analysis

. Binding-time analysis is a crucial part of offline partial evaluation. It is often specified as a non-standard type system. Many typebased binding-time analyses are reminiscent of simple type systems with additional features like recursive types. We make this connection explicit by expressing binding-time analysis with annotated type systems that separate the concerns of type inference from those of binding-time annotation. The separation enables us to explore a design space for bindingtime analysis by varying the underlying type system and the annotation strategy independently. The result is a classification of different monovariant binding-time analyses which allows us to compare their relative power. Due to the systematic approach we uncover some novel analyses. A partial evaluator separates the computation of a source program into two or more stages [7, 20]. Using the (static) input of the first stage it transforms a source program into a specialized residual program. Application..