A generic account of continuation-passing styles

ABSTRACT

We unify previous work on the continuation-passing style (CPS) transformations in a generic framework based on Moggi's computational meta-language. This framework is used to obtain CPS transformations for a variety of evaluation strategies and to characterize the corresponding administrative reductions and inverse transformations. We establish generic formal connections between operational semantics and equational theories. Formal properties of transformations for specific evaluation orders follow as corollaries. Essentially, we factor transformations through Moggi's computational m eta-language. Mapping &lgr;-terms into the meta-language captures computation properties (e.g., partiality, strictness) and evaluation order explicitly in both the term and the type structure of the meta-language. The CPS transformation is then obtained by applying a generic transformation from terms and types in the meta-language to CPS terms and types, based on a typed term representation of the continuation monad. We prove an adequacy property for the generic transformation and establish an equational correspondence between the meta-language and CPS terms. These generic results generalize Plotkin's seminal theorems, subsume more recent results, and enable new uses of CPS transformations and their inverses. We discuss how to aply these results to compilation.

REFERENCES

• 1: Andrew W. Appel, Compiling with continuations, Cambridge University Press, New York, NY, 1992
• 2: Henk Barendregt. The Lambda Calculus -- Its Syntax and Semantics. North-Holland, 1984.
• 3: Geoffrey Burn and Daniel Le M~tayer. Proving the correctness of compiler optimisations based on a global program analysis. Technical report Doc 92/20, Department of Computing, Imperial College of Science, Technology and Medicine, London, England, 1992.
• 4: William Clinger, editor. Proceed, ngs of the 1992 A CM Conference on Lisp and Functional Programmzng, LISP Pointers, Vol. V, No. 1, San Francisco, California, June 1992. ACM Press.
• 5: Olivier Danvy. Three steps for the CPS transformation. Technical Report CIS-92-2, Kansas State University, Manhattan, Kansas, December 1991.
• 6: Olivier Danvy, Back to direct style, Selected papers of the symposium on Fourth European symposium on programming, p.183-195, June 1994, Rennes, France
• 7: Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. In Wand {44}, pages 361-391.
• 8: Olivier Danvy , John Hatcliff, CPS-transformation after strictness analysis, ACM Letters on Programming Languages and Systems (LOPLAS), v.1 n.3, p.195-212, Sept. 1992 [doi>10.1145/151640.151641]
• 9: Olivier Danvy , John Hatcliff, On the Transformation between Direct and Continuation Semantics, Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, p.627-648, April 07-10, 1993
• 10: 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
• 11: Matthias Felleisen and Daniel P. Friedman. Control operators, the SECD machine, and the A-calculus. In M. Wirsing, editor, Formal Description of Programming Concepts III, pages 193-217. North-Holland, 1986.
• 12: Michael J. Fischer, Lambda calculus schemata, ACM SIGPLAN Notices, v.7 n.1, p.104-109, January 1972
• 13: Cormac Flanagan , Amr Sabry , Bruce F. Duba , Matthias Felleisen, The essence of compiling with continuations, ACM SIGPLAN Notices, v.28 n.6, p.237-247, June 1993
• 14: Timothy G. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-58, December 1989, San Francisco, California, United States [doi>10.1145/96709.96714]
• 15: Robert Harper , Mark Lillibridge, Polymorphic type assignment and CPS conversion, Lisp and Symbolic Computation, v.6 n.3-4, p.361-380, Nov. 1993 [doi>10.1007/BF01019463]
• 16: John Hatcliff. PhD thesis, Department of Computing and Information Sciences, Kansas State University, Manhattan, Kansas, USA, March 1994. Forthcoming.
• 17: John Hatcliff and Ohvier Danvy. Thunks and the )~- calculus. Technical Report CIS-93-15, Kansas State University, Manhattan, Kansas, September 1993.
• 18: P. Z. Ingerman, Thunks: a way of compiling procedure statements with some comments on procedure declarations, Communications of the ACM, v.4 n.1, p.55-58, Jan. 1961 [doi>10.1145/366062.366084]
• 19: Jufia L. Lawall. PhD thesis, Computer Science Department, Indiana University, Bloomington, Indiana, USA, 1993. Forthcoming.
• 20: Julia L. Lawall, Proofs by structural induction using partial evaluation, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.155-166, June 14-16, 1993, Copenhagen, Denmark [doi>10.1145/154630.154646]
• 21: Julia L. Lawall , Olivier Danvy, Separating stages in the continuation-passing style transformation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.124-136, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158613]
• 22: Albert R. Meyer , Mitchell Wand, Continuation Semantics in Typed Lambda-Calculi (Summary), Proceedings of the Conference on Logic of Programs, p.219-224, June 17-19, 1985
• 23: Eugenio Moggi. Computational lambda-calculus and monads. Report ECS-LFCS-88-66, University of Edinburgh, Edinburgh, Scotland, October 1988.
• 24: 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
• 25: Eugenio Moggi. An abstract view of programming languages. Course notes ECS-LFCS-90-113, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, Edinburgh, Scotland, April 1990.
• 26: Eugenio Moggi, Notions of computation and monads, Information and Computation, v.93 n.1, p.55-92, July 1991 [doi>10.1016/0890-5401(91)90052-4]
• 27: Luc Moreau , Daniel Ribbens, Sound rules for parallel evaluation of a functional language callcc, Proceedings of the conference on Functional programming languages and computer architecture, p.125-135, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165197]
• 28: Chetan Ram Murthy, Extracting constructive content from classical proofs, 1990
• 29: Alan Mycroft, The Theory and Practice of Transforming Call-by-need into Call-by-value, Proceedings of the Fourth 'Colloque International sur la Programmation' on International Symposium on Programming, p.269-281, April 22-24, 1980
• 30: J. W. Backus , F. L. Bauer , J. Green , C. Katz , J. McCarthy , A. J. Perlis , H. Rutishauser , K. Samelson , B. Vauquois , J. H. Wegstein , A. van Wijngaarden , M. Woodger , P. Naur, Revised report on the algorithm language ALGOL 60, Communications of the ACM, v.6 n.1, p.1-17, Jan. 1963 [doi>10.1145/366193.366201]
• 31: Chris Okasaki, Peter Lee, and David Tarditi. Call-byneed and continuation-passing style. In Talcott {39}.
• 32: Gordon D. Plotkin. Call-by-name, call-by-value and the )~-calculus. Theoretical Computer Science, 1:125-159, 1975.
• 33: 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]
• 34: John C. Reynolds, On the Relation between Direct and Continuation Semantics, Proceedings of the 2nd Colloquium on Automata, Languages and Programming, p.141-156, July 29-August 02, 1974
• 35: Amr Sabry , Matthias Felleisen, Reasoning about programs in continuation-passing style., ACM SIGPLAN Lisp Pointers, v.V n.1, p.288-298, Jan. 1992
• 36: Amr Sabry , Matthias Felleisen, Reasoning about programs in continuation-passing style, Lisp and Symbolic Computation, v.6 n.3-4, p.289-360, Nov. 1993 [doi>10.1007/BF01019462]
• 37: Amr Sabry and John Field. Reasoning about explicit and implicit representation of state. In Paul Hudak, editor, Proceedings of the A CM SIGPLAN Workshop on State in Programming Languages, pages 17-30, Copenhagen, Denmark, June 1993.
• 38: David A. Schmidt, Denotational semantics: a methodology for language development, William C. Brown Publishers, Dubuque, IA, 1986
• 39: Carolyn L. Talcott, editor. Special issue on continuations, LISP and Symbolic Computation, Vol. 6, Nos. 3/4. Kluwer Academic Publishers, 1993.
• 40: R. D. Tennent, Principles of Programming Languages, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 41: Philip Wadler, Comprehending monads, Proceedings of the 1990 ACM conference on LISP and functional programming, p.61-78, June 27-29, 1990, Nice, France [doi>10.1145/91556.91592]
• 42: Philip Wadler, The essence of functional programming, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143169]
• 43: Mitchell Wand, Correctness of Procedure Representations in Higher-Order Assembly Language, Proceedings of the 7th International Conference on Mathematical Foundations of Programming Semantics, p.294-311, March 25-28, 1991
• 44: Mitchell Wand, editor. Special issue on the 1990 A CM Conference on Lisp and Functional Programming, Mathematical Structures in Computer Science, Vol. 2, No. 4. Cambridge University Press, December 1992.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

General Terms:
Languages, Theory, Verification