View Full Document

Correctness of Binding-time Analysis



View the full content.
View Full Document
View Full Document

3 views

Unformatted text preview:

Journal of Functional Programming 1993 vol 3 3 pp 347 363 Correctness of Binding time Analysis Jens Palsberg palsberg daimi aau dk Computer Science Department Aarhus University Ny Munkegade DK 8000 Aarhus C Denmark Abstract A binding time analysis is correct if it always produces consistent binding time information Consistency prevents partial evaluators from going wrong A sufficient and decidable condition for consistency called well annotatedness was first presented by Gomard and Jones In this paper we prove that a weaker condition implies consistency Our condition is decidable subsumes the one of Gomard and Jones and was first studied by Schwartzbach and the present author Our result implies the correctness of the binding time analysis of Mogensen and it indicates the correctness of the core of the binding time analyses of Bondorf and Consel We also prove that all partial evaluators will on termination have eliminated all eliminable marked parts of an input which satisfies our condition This generalizes a result of Gomard Our development is for the pure calculus with explicit binding time annotations 1 Introduction A partial evaluator is an implementation of Kleene s Snm theorem When given a program and some of its expected input a partial evaluator produces a so called residual program The residual program will when given the remaining input produce the same result as would have the original program when given all of the input The challenge for a partial evaluator is to produce residual programs that are significantly faster than the input programs Partial evaluators can for example be used to generate compilers from interpreters Bondorf 1991 Gomard Jones 1991 Most partial evaluators use a binding time analysis in a pre processing phase A binding time analysis annotates a program by marking as eliminable those parts which may be evaluated during partial evaluation and by marking remaining parts as residual Partial evaluation then proceeds by attempting to



Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view Correctness of Binding-time Analysis and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Correctness of Binding-time Analysis and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?