Polymorphic Binding-Time Analysis

Fritz Henglein, Christian Mossin. Polymorphic Binding-Time Analysis. In Donald Sannella, editor, Programming Languages and Systems - ESOP 94, 5th European Symposium on Programming, Edinburgh, U.K., April 11-13, 1994, Proceedings. Volume 788 of Lecture Notes in Computer Science, pages 287-301, Springer, 1994. [doi]

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 analyses 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 notion of polyvariance limited only by the (standard) types of the language. Polymorphism gives a much simpler definition than the known polyvariant schemes allowing us to reason formally about the system and prove it correct. This paper is based on work in [14].