Correct flow analysis in continuation semantics

ABSTRACT

Three semantics-preserving transformations (static replacement, factoring, and combinator selection) are used to convert a continuation semantics into a formal description of a semantic analyzer and code generator. The result of this derivation is a compilation algorithm which performs type checking before code generation so that type-checking instructions are not generated in the target code. Both the flow analysis and the resulting optimizations are proved correct with respect to the original definition of the source language. The proof consists of showing that all restructuring transformations preserve the semantics of the source language. This transformational approach can be extended to derive correctness proofs of other flow analysis and code optimization techniques.

REFERENCES

• 1: Barbuti, R. and A. Martelli, (1983) "A Structured Ap~ proach to Static Semantics Correctness," Science of Computer Programming 3,3 223-321.
• 2: Donzeau-Gouge, V., (19'80) "Denotational Definition of Properties of Program Computations" in ,Program Flow Analysi.s: Theory and Applications edited by S. S. Muchnick and N. D. Jones. Englewood Cliifs, New Jersey: Prent~ce-Hali.
• 3: Paul Hudak , David Kranz, A combinator-based compiler for a functional language, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.122-132, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800523]
• 4: Neil D. Jones , Steven S. Muchnick, A fixed-program machine for combinator expression evaluation, Proceedings of the 1982 ACM symposium on LISP and functional programming, p.11-20, August 15-18, 1982, Pittsburgh, Pennsylvania, United States [doi>10.1145/800068.802130]
• 5: Ulrik Jørring , William L. Scherlis, Compilers and staging transformations, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.86-96, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512652]
• 6: Milner, R., (1978) "A Theory of Type Polymorphism in Programming," Journal of Computer and System Sciences 17, 348-375.
• 7: M M Montenyohl, Static analysis based on denotational transformations, Indiana University, Bloomington, IN, 1986
• 8: Nielson, F., (I982) "A Denotational Framework for Data Flow Analysis," Acta Informatica 18, 265-287.
• 9: Flemming Nielson, Program transformations in a denotational setting, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.3, p.359-379, July 1985 [doi>10.1145/3916.3917]
• 10: Pleban, U. F. and S. S. Muchnick, (1980) "A Denotational Semantics Approach to Program Optimization" Proceedings of the 1980 Conference on Information Sciences and System~ Princeton: Princeton University Dept. of EE and CS, 211-215.
• 11: Turner, D. A., (1979) "A New Implementation Technique for Applicative Lunguages," Software Practice and Experience 9, 31-49.
• 12: Wand, M., (1980) "Different Advice on Structuring Compilers and Proving Them Correct," Indiana University Computer Science Dept. Technical Report 95.
• 13: Mitchell Wand, Semantics-directed machine architecture, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.234-241, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582179]
• 14: Mitchell Wand, Deriving Target Code as a Representation of Continuation Semantics, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.496-517, July 1982 [doi>10.1145/357172.357179]
• 15: Mitchell Wand, Loops in combinator-based compilers, Information and Control, v.57 n.2-3, p.148-164, May/June 1983 [doi>10.1016/S0019-9958(83)80041-2]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Optimization

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers; Code generation

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures

General Terms:
Algorithms, Languages, Performance, Verification