Specifying the correctness of binding-time analysis

ABSTRACT

Mogensen has exhibited a very compact partial evaluator for the pure lambda calculus, using binding-time analysis followed by specialization. We give a correctness criterion for this partial evaluator and prove its correctness relative to this specification. We show that the conventional properties of partial evaluators, such as the Futamura projections, are consequences of this specification. By considering both a flow analysis and the transformation it justifies together, this proof suggests a framework for the incorporating flow analyses into verified compilers.

REFERENCES

• 1: Henk Barendregt. Self-Interpretation in Lambda Calculus. Journal of Functional Programming, 1(2):229-234, April 1991.
• 2: Charles Consel, Binding time analysis for high order untyped functional languages, Proceedings of the 1990 ACM conference on LISP and functional programming, p.264-272, June 27-29, 1990, Nice, France [doi>10.1145/91556.91668]
• 3: Charles Consel and Siau Cheng Khoo. On-lilie &" Off-line Partial Evaluation: Semantic Specifications and Correctness Proofs. Technical Report YALEU/DCS/RR-912, Yale University Department of Computer Science, June 1992.
• 4: Carsten K. Gomard, Partial type inference for untyped functional programs, Proceedings of the 1990 ACM conference on LISP and functional programming, p.282-287, June 27-29, 1990, Nice, France [doi>10.1145/91556.91672]
• 5: Carsten K. Gomard, A self-applicable partial evaluator for the lambda calculus: correctness and pragmatics, ACM Transactions on Programming Languages and Systems (TOPLAS), v.14 n.2, p.147-172, April 1992 [doi>10.1145/128861.128864]
• 6: Sebastian Hunt , David Sands, Binding time analysis: a new PERspective, ACM SIGPLAN Notices, v.26 n.9, p.154-165, Sept. 1991
• 7: 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]
• 8: John Launchbury. Projection Factorizations in Partial Evaluation. PhD thesis, University of Glasgow, November 1989.
• 9: John Launchbury, A strongly-typed self-applicable partial evaluator, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.145-164, June 1991, Cambridge, Massachusetts, United States
• 10: Torben ~F,. Mogensen. Efficient Self-Interpretation in Lambda Calculus. to appear, .June 1992.
• 11: Torben A3. Mogensen. Self-applicable Partial Evaluation for Pure Lambd~ Calculus. In Charles Consel, editor, A CM SIGPLAN Workshop on Partial Evaluation and Se~nantics-Based Program Manipulation. pages 116-121, 199'2.
• 12: 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]
• 13: F. Pfenning , C. Elliot, Higher-order abstract syntax, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.199-208, June 20-24, 1988, Atlanta, Georgia, United States

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

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

General Terms:
Algorithms, Languages, Theory, Verification