Abstract
Binding-time analysis is a crucial part of offline partial evaluation. It is often specified as a non-standard type system. Many type-based 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 binding-time analysis by varying the underlying type system and the annotation strategy independently. The result is a classification of different mono-variant binding-time analyses which allows us to compare their relative power. Due to the systematic approach we uncover some novel analyses.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. M. Amadio and L. Cardelli. Subtyping recursive types. ACM Trans. Prog. Lang. Syst., 15(4):575–631, 1993.
L. Birkedal and M. Welinder. Binding-time analysis for Standard-ML. In P. Sestoft and H. SØndergaard, editors, Proc. ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation PEPM '94, pages 61–71, Orlando, Fla., June 1994. ACM.
A. Bondorf. Automatic autoprojection of higher order recursive equations. Science of Programming, 17:3–34, 1991.
A. Bondorf and J. JØrgensen. Efficient analysis for realistic off-line partial evaluation. Journal of Functional Programming, 3(3):315–346, July 1993.
C. Consel. Binding time analysis for higher order untyped functional languages. In LFP 1990 [23], pages 264–272.
C. Consel. Polyvariant binding-time analysis for applicative languages. In D. Schmidt, editor, Proc. ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation PEPM '93, pages 66–77, Copenhagen, Denmark, June 1993. ACM Press.
C. Consel and O. Danvy. Tutorial notes on partial evaluation. In Proc. 20th Annual ACM Symposium on Principles of Programming Languages, pages 493–501, Charleston, South Carolina, Jan. 1993. ACM Press.
O. Danvy. Type-directed partial evaluation. In Proc. 23rd Annual ACM Symposium on Principles of Programming Languages, pages 242–257, St. Petersburg, Fla., Jan. 1996. ACM Press.
O. Danvy, K. MalmkjÆr, and J. Palsberg. The essence of eta-expansion in partial evaluation. Lisp and Symbolic Computation, 8(3):209–227, July 1995.
O. Danvy, K. MalmkjÆr, and J. Palsberg. Eta-expansion does The Trick. Technical Report BRICS RS-95-41, Computer Science Dept., Aarhus University, Denmark, Aug. 1995.
R. Di Cosmo and D. Kesner. Simulating expansions without expansions. Mathematical Structures in Computer Science, 4:1–48, 1994.
D. Dussart, F. Henglein, and C. Mossin. Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial time. In Mycroft [26], pages 118–136.
R. Glück and J. JØrgensen. Fast multi-level binding-time analysis for multiple program specialization. In PSI '96 [31].
C. K. Gomard. Partial type inference for untyped functional programs. In LFP 1990 [23], pages 282–287.
C. K. Gomard and N. D. Jones. A partial evaluator for the untyped lambda-calculus. Journal of Functional Programming, 1(1):21–70, Jan. 1991.
N. Heintze. Set-based analysis of ML-programs. In Proc. 1994 ACM Conference on Lisp and Functional Programming, pages 306–317, Orlando, Florida, USA June 1994. ACM Press.
N. Heintze. Control-flow analysis and type systems. In Mycroft [26], pages 189–206. LNCS 983.
F. Henglein. Efficient type inference for higher-order binding-time analysis. In J. Hughes, editor, Proc. Functional Programming Languages and Computer Architecture 1991, pages 448–472, Cambridge, MA, 1991. Springer-Verlag. LNCS 523.
J. E. Hopcroft and J. D. Ullman. Introduction to automata theory, languages and computation. Addison-Wesley, 1979.
N. D. Jones, C. K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall, 1993.
N. D. Jones, P. Sestoft, and H. SØndergaard. An experiment in partial evaluation: The generation of a compiler generator. In J.-P. Jouannaud, editor, Rewriting Techniques and Applications, pages 124–140, Dijon, France, 1985. Springer-Verlag. LNCS 202.
J. Launchbury. Projection Factorisations in Partial Evaluation, volume 1 of Distinguished Dissertations in Computer Science. Cambridge University Press, 1991.
Proc. 1990 ACM Conference on Lisp and Functional Programming, Nice, France, 1990. ACM Press.
K. Malmkjser, O. Danvy, and N. Heintze. ML partial evaluation using set-based analysis. In Record of the ACM-SIGPLAN Workshop on ML and its Applications, number 2265 in INRIA Research Report, pages 112–119, BP 105, 78153 Le Chesnay Cedex, France, June 1994.
T. Æ. Mogensen. Self-applicable partial evaluation for pure lambda calculus. In C. Consel, editor, Proc. ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation PEPM '92, pages 116–121, San Francisco, CA, June 1992. Yale University. Report YALEU/DCS/RR-909.
A. Mycroft, editor. Proc. International Static Analysis Symposium, SAS'95, Glasgow, Scotland, Sept. 1995. Springer-Verlag. LNCS 983.
F. Nielson and H. R. Nielson. Two-Level Functional Languages. Cambridge University Press, 1992.
F. Nielson and H. R. Nielson. Multi-level lambda-calculi: an algebraic description. In O. Danvy, R. Glück, and P. Thiemann, editors, Partial Evaluation, volume 1110 of Lecture Notes in Computer Science, pages 338–354, Dagstuhl, Germany, Feb. 1996. Springer Verlag, Heidelberg.
J. Palsberg and P. O'Keefe. A type system equivalent to flow analysis. In Proc. 22nd Annual ACM Symposium on Principles of Programming Languages, pages 367–378, San Francisco, CA, Jan. 1995. ACM Press.
J. Palsberg and M. I. Schwartzbach. Binding-time analysis: Abstract interpretation versus type inference. In IEEE International Conference on Computer Languages 1994, pages 289–298, Toulouse, France, 1994. IEEE Computer Society Press.
PSI-96: Andrei Ershov Second International Memorial Conference, Perspectives of System Informatics, volume 1181 of Lecture Notes in Computer Science, Novosibirsk, Russia, June 1996. Springer-Verlag.
H. Seidl. Least solutions of equations over N. In Proc. International Conference of Automata, Languages and Programming, ICALP '94, volume 820 of Lecture Notes in Computer Science, pages 400–411. Springer-Verlag, 1994.
K. L. Solberg. Annotated Type Systems for Program Analysis. PhD thesis, Odense University, Denmark, July 1995. Also technical report DAIMI PB-498, Comp. Sci. Dept. Aarhus University.
P. Thiemann. Towards partial evaluation of full Scheme. In G. Kiczales, editor, Reflection'96, pages 95–106, San Francisco, CA, USA, Apr. 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Thiemann, P. (1997). A unified framework for binding-time analysis. In: Bidoit, M., Dauchet, M. (eds) TAPSOFT '97: Theory and Practice of Software Development. CAAP 1997. Lecture Notes in Computer Science, vol 1214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0030638
Download citation
DOI: https://doi.org/10.1007/BFb0030638
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62781-4
Online ISBN: 978-3-540-68517-3
eBook Packages: Springer Book Archive