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

  • Anindya Banerjee
  • Nevin Heintze
  • Jon G. Riecke
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2215)


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.


Free Variable Target Language Operational Semantic Recursive Function Function Label 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Abadi, A. Banerjee, N. Heintze, and J.G. Riecke. A core calculus of dependency. In POPL’99, ACM Press.Google Scholar
  2. 2.
    A. Aho, R. Sethi, and J. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley Publishing Co., 1986.Google Scholar
  3. 3.
    A.W. Appel. Compiling with Continuations.Cambridge University Press, 1992.Google Scholar
  4. 4.
    A. Banerjee. A modular, polyvariant and type-based closure analysis.In ICFP’97, ACM Press.Google Scholar
  5. 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. 6.
    U. Boquist. Code Optimisation Techniques for Lazy Functional Languages.PhD thesis, Chalmers University of Technology, Goteborg University, 1999.Google Scholar
  7. 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. 8.
    H. Cejtin, S. Jagannathan, and S. Weeks. Flow-directed closure conversion for typed languages (Extended Summary). Available from URL:, 2000.
  9. 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. 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. 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. 12.
    C. Flanagan and M. Felleisen. Componential set-based analysis. In ACM Trans. on Programming Languages and Systems, 21(2):370–416, March 1999.CrossRefGoogle Scholar
  13. 13.
    C.A. Gunter. Semantics of Programming Languages.MIT Press, 1992.Google Scholar
  14. 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. 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. 16.
    N. Heintze and J.G. Riecke. The SLam calculus: programming with secrecy and integrity.In POPL’98, ACM Press.Google Scholar
  17. 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. 18.
    S. Jagannathan and S. Weeks. A unified treatment of flow analysis in higher-order languages.In POPL’95, ACM Press.Google Scholar
  19. 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. 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. 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. 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. 23.
    Y. Minamide, G. Morrisett and R. Harper. Typed Closure Conversion. In POPL’96, ACM Press.Google Scholar
  24. 24.
    J.C. Mitchell. Foundations for Programming Languages. MIT Press, 1996.Google Scholar
  25. 25.
    S.S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann, 1997.Google Scholar
  26. 26.
    L.R. Nielsen. A Denotational Investigation of Defunctionalization. Progress Report, BRICS Ph.D. School, June 1998.Google Scholar
  27. 27.
    F. Nielson. Program transformations in a denotational setting. ACM Trans. on Programming Languages and Systems, 7(3):359–379, 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  28. 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. 29.
    F. Nielson, H.R. Nielson and C. Hankin. Principles of Program Analysis.Springer-Verlag, 1999.Google Scholar
  30. 30.
    J. Palsberg. Closure analysis in constraint form. ACM Trans. on Programming Languages and Systems, 17(1):47–62, 1995.CrossRefGoogle Scholar
  31. 31.
    G.D. Plotkin. LCF considered as a programming language. Theoretical Computer Sci., 5:223–257, 1977.CrossRefMathSciNetGoogle Scholar
  32. 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. 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. 34.
    J.C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation, 11(4):363–397, December 1998.zbMATHCrossRefGoogle Scholar
  35. 35.
    J.C. Reynolds. Definitional interpreters revisited. Higher-Order and Symbolic Computation, 11(4):355–361, December 1998.zbMATHCrossRefGoogle Scholar
  36. 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.CrossRefGoogle Scholar
  37. 37.
    P. Sestoft. Replacing function parameters by global variables. Master’s thesis, DIKU, University of Copenhagen, Denmark, October 1988.Google Scholar
  38. 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. 39.
    P.A. Steckler and M. Wand. Lightweight closure conversion. ACM Trans. Programming Languages and Systems, 19(1):48–86, January 1997.CrossRefGoogle Scholar
  40. 40.
    M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2):109–176, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  41. 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.zbMATHCrossRefGoogle Scholar
  42. 42.
    M. Wand. Specifying the Correctness of Binding-Time Analysis.In Journal of Functional Programming, 3(3):365–387, July 1993.MathSciNetCrossRefGoogle Scholar
  43. 43.
    M. Wand and W. Clinger. Set Constraints for Destructive Array Update Optimization. In Journal of Functional Programming, 2000, to appear.Google Scholar
  44. 44.
    M. Wand and I. Siveroni. Constraint systems for useless variable elimination. In POPL’99, ACM Press.Google Scholar
  45. 45.
    D. Wang and A. Appel. Type-preserving garbage collectors. In POPL’01, ACM Press.Google Scholar
  46. 46.
    K. Yi. An abstract interpretation for estimating uncaught exceptions in Standard ML programs. In Science of Computer Programming, 31(1):147–173, 1998.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Anindya Banerjee
    • 1
  • Nevin Heintze
    • 2
  • Jon G. Riecke
    • 3
  1. 1.Kansas State UniversityManhattanUSA
  2. 2.Agere SystemsMurray HillUSA
  3. 3.Aleri, Inc.New YorkUSA

Personalised recommendations