The correctness of an optimized code generation

ABSTRACT

For a functional programming language with a lazy standard semantics, we define a strictness analysis by means of abstract interpretation. Using the information from the strictness analysis we are able to define a code generation which avoids delaying the evaluation of the argument to an application, provided that the corresponding function is strict. To show the correctness of the code generation, we will adopt the framework of logical relations and define a layer of predicates which finally will ensure that the code generation is correct with respect to the standard semantics.

REFERENCES

• 1: Samson Abrarasky and Chris Hankin. An introduction to abstrax:t interpretation. In Samson Abramsky and Chris Hankin, editors, Abstract Interpretation o/ Declarative Languages, chapter 1, pages 9-31. Ellis Hotwood, 1987.
• 2: Hans Bekic, Definable Operation in General Algebras, and the Theory of Automata and Flowcharts, Programming Languages and Their Definition - Hans Bekic (1936-1982), p.30-55, January 1984
• 3: G. L. Burn, Using projection analysis of evaluation-order and its application, Proceedings of the 1990 ACM conference on LISP and functional programming, p.227-240, June 27-29, 1990, Nice, France [doi>10.1145/91556.91655]
• 4: G. L. Burn, The evaluation transformer model of reduction and its correctness, Proceedings of the international joint conference on theory and practice of software development on Advances in distributed computing (ADC) and colloquium on combining paradigms for software development (CCPSD): Vol. 2, p.458-482, April 1991, Brighton, United Kingdom
• 5: Geoffrey Burn, Lazy functional languages: abstract interpretation and compilation, MIT Press, Cambridge, MA, 1991
• 6: Geoffrey L. Burn, Chris Hankin, and Samson Abramsky. Strictness analysis for higher-order functions. Science of Computer Programming, 7:249-278, 1986.
• 7: P. Cousot and R. Cousot. Abstract Interpretation Frameworks. Journal of Logic and Computation, 2(4):511-547, August 1992.
• 8: P Dybjer, Using domain algebras to prove the correctness of a compiler, Proceedings on STACS 85 2nd annual symposium on theoretical aspects of computer science, p.98-108, December 1985, Saarbru:9Aicken, Germany
• 9: Pascal Fradet , Daniel Le Métayer, Compilation of functional languages by program transformation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.1, p.21-51, Jan. 1991 [doi>10.1145/114005.102805]
• 10: Mike Gordon. HOL- A Proof Generating System for Higher-Order Logic. Cambridge CL TR 103, Computer Laboratory, University of Cambridge, 1987.
• 11: John Hannan , Dale Miller, From operational semantics to abstract machines: preliminary results, Proceedings of the 1990 ACM conference on LISP and functional programming, p.323-332, June 27-29, 1990, Nice, France [doi>10.1145/91556.91680]
• 12: Paul Hudak , Jonathan Young, Higher-order strictness analysis in untyped lambda calculus, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-109, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512653]
• 13: Torben P. Lunge. Implementation af paxametriserede semantikker, 1990. Report of written project, Aaxhus University, Denmark. In Danish.
• 14: Torben P. Lunge. Correctness of Code Generations Based on a Functional Programming Language. Master's thesis, Aarhus University, Denmark, 1992.
• 15: F. Lockwood Morris, Advice on structuring compilers and proving them correct, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.144-152, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512941]
• 16: Flemming Nielson , Hanne Riis Nielson, Two-level semantics and code generation, Theoretical Computer Science, v.56 n.1, p.59-133, Jan. 1988 [doi>10.1016/0304-3975(86)90006-X]
• 17: Hanne Riis Nielson , Flemming Nielson, Context information for lazy code generation, Proceedings of the 1990 ACM conference on LISP and functional programming, p.251-263, June 27-29, 1990, Nice, France [doi>10.1145/91556.91665]
• 18: Flemming Nielson , Hanne Riis Nielson, Layered Predicates, Proceedings of the REX Workshop on Sematics: Foundations and Applications, p.425-456, June 01-04, 1992
• 19: Flemming Nielson , Hanne Riis Nielson, Two-level functional languages, Cambridge University Press, New York, NY, 1992
• 20: Lawrence C. Paulson. Experience with Isabelle: A Generic Theorem Prover. Cambridge TR 143, Computer Laboratory, University of Cambridge, 1988. Preliminary version.
• 21: Gordon D. Plotkin. Lambda-definability and logical relations. Memorandum SAI-RM-4, School of Artificial Intelligence, University of Edinburgh, 1973.
• 22: Gordon D. Plotkin. Lambda-definabifity in the full type hierarchy. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.
• 23: J. C. Reynolds. Types, Abstraction and Parametric Polymorphism. in Proceedings in Information Processing (1FIP}, pages 513-523. North-Holland, 1983.
• 24: J. E. Stay. The Congruence of two Programming Language Definitions. Theoretical Computer Science, 13:151-174, 1981.
• 25: J. W. Thatcher, E. G. Wagner, and J. B. Wright. More on advice on structuring compilers and proving them correct. Theoretical Computer Science, 15:223- 249, 1981.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Procedures, functions, and subroutines
      D.3.4 Processors
          Subjects: Code generation

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Algorithms, Languages, Verification