A unified framework for binding-time analysis

Abstract

Binding-time analysis is a crucial part of o~ine 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 bindingtimeanalysis by varying the underlying type system and the annotation strategy independently. The result is a classification of different monova~ iant binding-time analyses which allows us to compare their relative power. Due to the systematic approach we uncover some novel analyses.