Slightly Revised Version Polymorphic Binding-Time Analysis

Abstract. Binding time analysis is an important part of off-line partial evaluation, annotating expressions as being safely evaluable from known data or possibly depending on unknown data. Most binding-time analy-ses have been monovariant, allowing only one binding-time description for each function. The idea of polyvariance is to allow multiple binding time descriptions of each function, by duplicating the function [6, 2] or by associating a set of binding time descriptions to each function [3]. Instead we present an inference based binding time analysis polymorphic in binding time values. This polymorphism captures a very powerful no-tion of polyvariance limited only by the (standard) types of the language. Polymorphism gives a much simpler definition than the known polyvari-ant schemes allowing us to reason formally about the system and prove it correct. This paper is based on work in [14].