Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Theoretical Aspects of Computer Software

TACS 2001: Theoretical Aspects of Computer Software pp 420–447Cite as

Design and Correctness of Program Transformations Based on Control-Flow Analysis

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2215))

Abstract

We show how control-flow-based program transformations in functional languages can be proven correct. The method relies upon “defunctionalization,” a mapping from a higher-order language to a first-order language.W e first show that defunctionalization is correct; using this proof and common semantic techniques, we then show how two program transformations — flow-based inlining and lightweight defunctionalization — can be proven correct.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi, A. Banerjee, N. Heintze, and J.G. Riecke. A core calculus of dependency. In POPL’99, ACM Press.

    Google Scholar 

  2. A. Aho, R. Sethi, and J. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley Publishing Co., 1986.

    Google Scholar 

  3. A.W. Appel. Compiling with Continuations.Cambridge University Press, 1992.

    Google Scholar 

  4. A. Banerjee. A modular, polyvariant and type-based closure analysis.In ICFP’97, ACM Press.

    Google Scholar 

  5. H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic.North-Holland, 1981.Revised Edition, 1984.

    Google Scholar 

  6. U. Boquist. Code Optimisation Techniques for Lazy Functional Languages.PhD thesis, Chalmers University of Technology, Goteborg University, 1999.

    Google Scholar 

  7. H. Cejtin, S. Jagannathan, and S. Weeks. Flow-directed closure conversion for typed languages.In ESOP 2000, number 1782 in Lect.Notes in Computer Sci. Springer-Verlag.

    Google Scholar 

  8. H. Cejtin, S. Jagannathan, and S. Weeks. Flow-directed closure conversion for typed languages (Extended Summary). Available from URL:http://www.neci.nj.nec.com/homepages/jagannathan/publications.html, 2000.

  9. J. Dean, G. DeFouw, D. Grove, and C. Chambers. Vortex: An Optimizing Compiler for Object-Oriented Languages.In OOPSLA’96, ACM Press.

    Google Scholar 

  10. A. Dimock, R. Muller, F. Turbak, and J.B. Wells. Strongly typed flow-directed representation transformations.In ICFP’97, ACM Press.

    Google Scholar 

  11. M. Fahndrich and A. Aiken. Making set-constraint based program analyses scale. Technical Report 96-917, University of California, Berkeley, Computer Science Division, 1996.

    Google Scholar 

  12. C. Flanagan and M. Felleisen. Componential set-based analysis. In ACM Trans. on Programming Languages and Systems, 21(2):370–416, March 1999.

    Article  Google Scholar 

  13. C.A. Gunter. Semantics of Programming Languages.MIT Press, 1992.

    Google Scholar 

  14. J. Hannan. Type systems for closure conversion. In H.R. Nielson and K.L. Solberg, editors, Proceedings of the Workshop on Types in Program Analysis. Technical Report PB-493, University of Aarhus, 1995.

    Google Scholar 

  15. N. Heintze. Control-flow analysis and type systems.In SAS’95, number 983 in Lect.Notes in Computer Sci. Springer-Verlag.

    Google Scholar 

  16. N. Heintze and J.G. Riecke. The SLam calculus: programming with secrecy and integrity.In POPL’98, ACM Press.

    Google Scholar 

  17. U. Holzle and O. Agesen. Dynamic vs.static optimization techniques for objectoriented languages. Theory and Practice of Object Systems, 1(3), 1996.

    Google Scholar 

  18. S. Jagannathan and S. Weeks. A unified treatment of flow analysis in higher-order languages.In POPL’95, ACM Press.

    Google Scholar 

  19. S. Jagannathan and A. Wright. Effective flow analysis for avoiding runtime checks. In SAS’95, number 983 in Lect.Notes in Computer Sci. Springer-Verlag.

    Google Scholar 

  20. N.D. Jones. Flow analysis of lambda expressions (preliminary version). In S. Even and O. Kariv, editors, Automata, Languages and Programming: Eighth Colloquium, volume 115 of Lect. Notes in Computer Sci., pages 114–128.Springer-Verlag, July 1981.

    Google Scholar 

  21. G. Kahn. Natural semantics.In Proceedings Symposium on Theoretical Aspects of Computer Science, volume 247 of Lect. Notes in Computer Sci., New York, 1987. Springer-Verlag.

    Google Scholar 

  22. N. Kobayashi. Type-based useless variable elimination. In ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, pages 84–93, ACM, 2000.

    Google Scholar 

  23. Y. Minamide, G. Morrisett and R. Harper. Typed Closure Conversion. In POPL’96, ACM Press.

    Google Scholar 

  24. J.C. Mitchell. Foundations for Programming Languages. MIT Press, 1996.

    Google Scholar 

  25. S.S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann, 1997.

    Google Scholar 

  26. L.R. Nielsen. A Denotational Investigation of Defunctionalization. Progress Report, BRICS Ph.D. School, June 1998.

    Google Scholar 

  27. F. Nielson. Program transformations in a denotational setting. ACM Trans. on Programming Languages and Systems, 7(3):359–379, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  28. F. Nielson and H.R. Nielson. Infinitary control flow analysis: a collecting semantics for closure analysis.In POPL’97, ACM Press.

    Google Scholar 

  29. F. Nielson, H.R. Nielson and C. Hankin. Principles of Program Analysis.Springer-Verlag, 1999.

    Google Scholar 

  30. J. Palsberg. Closure analysis in constraint form. ACM Trans. on Programming Languages and Systems, 17(1):47–62, 1995.

    Article  Google Scholar 

  31. G.D. Plotkin. LCF considered as a programming language. Theoretical Computer Sci., 5:223–257, 1977.

    Article  MathSciNet  Google Scholar 

  32. J.C. Reynolds. Definitional interpreters for higher-order programming languages. In Proceedings of the ACM National Meeting (Boston, 1972), pages 717–740, 1972.

    Google Scholar 

  33. J.C. Reynolds. Types, abstraction and parametric polymorphism. In R.E.A. Mason, editor, Information Processing 83, pages 513–523. North Holland, Amsterdam, 1983.

    Google Scholar 

  34. J.C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation, 11(4):363–397, December 1998.

    Article  MATH  Google Scholar 

  35. J.C. Reynolds. Definitional interpreters revisited. Higher-Order and Symbolic Computation, 11(4):355–361, December 1998.

    Article  MATH  Google Scholar 

  36. D. Scott. A type theoretical alternative to CUCH, ISWIM, OWHY. Theoretical Computer Science, 121:411–440.Published version of unpublished manuscript, Oxford University, 1969.

    Article  Google Scholar 

  37. P. Sestoft. Replacing function parameters by global variables. Master’s thesis, DIKU, University of Copenhagen, Denmark, October 1988.

    Google Scholar 

  38. O. Shivers. Control-flow analysis of higher-order languages.PhD thesis, School of Computer Science, Carnegie Mellon University, 1991. Available as Technical Report CMU-CS-91-145.

    Google Scholar 

  39. P.A. Steckler and M. Wand. Lightweight closure conversion. ACM Trans. Programming Languages and Systems, 19(1):48–86, January 1997.

    Article  Google Scholar 

  40. M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2):109–176, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  41. A. Tolmach and D.P. Oliva. From ML to Ada: Strongly-typed language interoperability via source translation. Journal of Functional Programming, 8(4):367–412, July 1998.

    Article  MATH  Google Scholar 

  42. M. Wand. Specifying the Correctness of Binding-Time Analysis.In Journal of Functional Programming, 3(3):365–387, July 1993.

    Article  MathSciNet  Google Scholar 

  43. M. Wand and W. Clinger. Set Constraints for Destructive Array Update Optimization. In Journal of Functional Programming, 2000, to appear.

    Google Scholar 

  44. M. Wand and I. Siveroni. Constraint systems for useless variable elimination. In POPL’99, ACM Press.

    Google Scholar 

  45. D. Wang and A. Appel. Type-preserving garbage collectors. In POPL’01, ACM Press.

    Google Scholar 

  46. K. Yi. An abstract interpretation for estimating uncaught exceptions in Standard ML programs. In Science of Computer Programming, 31(1):147–173, 1998.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Kansas State University, Manhattan, KS, 66506, USA

    Anindya Banerjee

  2. Agere Systems, Murray Hill, NJ, 07974, USA

    Nevin Heintze

  3. Aleri, Inc., New York, NY, 10011, USA

    Jon G. Riecke

Authors
  1. Anindya Banerjee
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nevin Heintze
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jon G. Riecke
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Tokyo Institute of Technology Graduate School of Information Science and Engineering, 2-12-1 Oo-okayama, Meguro-ku, Tokyo, 152-8552, Japan

    Naoki Kobayashi

  2. Department of Computer and Information Science, University of Pennsylvania, 200 S. 33rd St., Philadelphia, PA, 19104, USA

    Benjamin C. Pierce

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Banerjee, A., Heintze, N., Riecke, J.G. (2001). Design and Correctness of Program Transformations Based on Control-Flow Analysis. In: Kobayashi, N., Pierce, B.C. (eds) Theoretical Aspects of Computer Software. TACS 2001. Lecture Notes in Computer Science, vol 2215. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45500-0_21

Download citation

  • DOI: https://doi.org/10.1007/3-540-45500-0_21

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42736-0

  • Online ISBN: 978-3-540-45500-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation