Reasoning about programs in continuation-passing style.

ABSTRACT

Plotkin's &lgr;-value calculus is sound but incomplete for reasoning about &bgr;eegr;-transformations on programs in continuation-passing style (CPS). To find a complete extension, we define a new, compactifying CPS transformation and an “inverse”mapping, un-CPS, both of which are interesting in their own right. Using the new CPS transformation, we can determine the precise language of CPS terms closed under &bgr;7eegr;-transformations. Using the un-CPS transformation, we can derive a set of axioms such that every equation between source programs is provable if and only if &bgr;&eegr; can prove the corresponding equation between CPS programs. The extended calculus is equivalent to an untyped variant of Moggi's computational &lgr;-calculus.

REFERENCES

• 1: A. W. Appel , T. Jim, Continuation-passing, closure-passing style, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.293-302, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75303]
• 2: BARENDREGT, H.P. The Lambda Calculus: Its Syntaz and Semantics. Revised Edition. Studies in Logic and the Foundations of Mathematics 103. North-Holland, Amsterdam, 1984.
• 3: Olivier Danvy, Back to direct style, Symposium proceedings on 4th European symposium on programming, p.130-150, January 1992, Rennes, France
• 4: DANVY, O. Three steps for the CPS transformation. Tech. Rep. CIS-92-2. Kansas State University, 1992.
• 5: DANVY, O. AND A. FILINSKI. Representing control: A study of the CPS transformation. Tech. Rpt. CIS-91-2. Kansas State University, 1991.
• 6: Olivier Danvy , Julia L. Lawall, Back to direct style II: first-class continuations, Proceedings of the 1992 ACM conference on LISP and functional programming, p.299-310, June 22-24, 1992, San Francisco, California, United States
• 7: FELLC. ISEN, M. AND D.P. FRIEDMAN. Control operators, the SECD-machine, and the A-calculus. In Formal Description of Programming Concepts III, edited by M. Wirsing. Elsevier Science Publishers B.V. (North-Holland), Amsterdam, 1986, 193-217.
• 8: Matthias Felleisen , Robert Hieb, The revised report on the syntactic theories of sequential control and state, Theoretical Computer Science, v.103 n.2, p.235-271, 14 Sept. 1992 [doi>10.1016/0304-3975(92)90014-7]
• 9: M. Felleisen , D. P. Friedman , E. Kohlbecker , B. Duba, A syntactic theory of sequential control, Theoretical Computer Science, v.52 n.3, p.205-237, June 1987 [doi>10.1016/0304-3975(87)90109-5]
• 10: Michael J. Fischer, Lambda calculus schemata, ACM SIGPLAN Notices, v.7 n.1, p.104-109, January 1972
• 11: John Gateley , Bruce F. Duba, Call-by-Value Combinatory Logic and the Lambda-Value Calculus, Proceedings of the 7th International Conference on Mathematical Foundations of Programming Semantics, p.41-53, March 25-28, 1991
• 12: R. Hieb , R. Kent Dybvig , Carl Bruggeman, Representing control in the presence of first-class continuations, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.66-77, June 1990, White Plains, New York, United States
• 13: David Kranz , Norman Adams , Richard Kelsey , Jonathan Rees , Paul Hudak , James Philbin, ORBIT: an optimizing compiler for scheme, ACM SIGPLAN Notices, v.21 n.7, p.219-233, July 1986
• 14: LANDIN, P.J. The mechanical evaluation of expressions. Comput. J. 6(4), 1964, 308-320.
• 15: LEaOY, X. The Zinc experiement. Technical Report 117. iNRIA, 1990.
• 16: E. Moggi, Computational lambda-calculus and monads, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.14-23, June 1989, Pacific Grove, California, United States
• 17: PLOTKIN, G.D. Call-by-name, call-by-value, and the A-calculus. Theor. Comput. Sci. 1, 1975, 125- 159.
• 18: John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800194.805852]
• 19: Olin Grigsby Shivers, Control-flow analysis of higher-order languages of taming lambda, Carnegie Mellon University, Pittsburgh, PA, 1991
• 20: Guy L. Steele, Jr., Rabbit: A Compiler for Scheme, Massachusetts Institute of Technology, Cambridge, MA, 1978

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Control primitives

General Terms:
Languages, Theory