Hostname: page-component-6bf8c574d5-gr6zb Total loading time: 0 Render date: 2025-02-21T02:49:45.654Z Has data issue: false hasContentIssue false
  • English
  • Français

On one-pass CPS transformations

Published online by Cambridge University Press:  01 November 2007

OLIVIER DANVY ,
KEVIN MILLIKIN  and
LASSE R. NIELSEN
OLIVIER DANVY
Affiliation:
BRICS, Department of Computer Science, University of Aarhus, IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark email: [email protected], [email protected], [email protected]
KEVIN MILLIKIN
Affiliation:
BRICS, Department of Computer Science, University of Aarhus, IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark email: [email protected], [email protected], [email protected]
LASSE R. NIELSEN
Affiliation:
BRICS, Department of Computer Science, University of Aarhus, IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark email: [email protected], [email protected], [email protected]
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We bridge two distinct approaches to one-pass CPS transformations, i.e, CPS transformations that reduce administrative redexes at transformation time instead of in a post-processing phase. One approach is compositional and higher-order, and is independently due to Appel, Danvy and Filinski, and Wand, building on Plotkin's seminal work. The other is non-compositional and based on a reduction semantics for the lambda-calculus, and is due to Sabry and Felleisen. To relate the two approaches, we use three tools: Reynolds's defunctionalization and its left inverse, refunctionalization; a special case of fold–unfold fusion due to Ohori and Sasano, fixed-point promotion; and an implementation technique for reduction semantics due to Danvy and Nielsen, refocusing. This work is directly applicable to transforming programs into monadic normal form.

Type
Article
Information
Journal of Functional Programming , Volume 17 , Issue 6 , November 2007 , pp. 793 - 812
Copyright
Copyright © Cambridge University Press 2007

References

Allison, L. (1986) A Practical Introduction to Denotational Semantics. New York, NY: Cambridge University Press.Google Scholar
Appel, A. W. (1992) Compiling With Continuations. New York, NY: Cambridge University Press.Google Scholar
Appel, A. W. & Jim, T. (1989) Continuation-passing, closure-passing style. In Proceedings of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, O'Donnell, M. J. & Feldman, S. (eds), Austin, TX: ACM Press, pp. 293–302.Google Scholar
Barendregt, H. (1984). The Lambda Calculus: Its Syntax and Semantics. Rev. ed. Studies in Logic and the Foundation of Mathematics, vol. 103. Amsterdam, The Netherlands, North-Holland.CrossRefGoogle Scholar
Barthe, G., Hatcliff, J. & Sørensen, M. H. (1999) CPS translations and applications: The cube and beyond. Higher-Order Symbolic Comput. 12 (2), 125–170.CrossRefGoogle Scholar
Benton, N. & Kennedy, A. (1999, Sept.) Monads, effects, and transformations. In Third International Workshop on Higher-Order Operational Techniques in Semantics. newblock Electronic Notes in Theoretical Computer Science, vol. 26, pp. 19–31. Elsevier, Paris, France.CrossRefGoogle Scholar
Biernacka, M. & Danvy, O. (in press) A concrete framework for environment machines. ACM Trans. Computat. Logic. Available as the technical report BRICS RS-06-3.Google Scholar
Biernacka, M. & Danvy, O. (2006a, Dec.) A Syntactic Correspondence Between Context-Sensitive Calculi and Abstract Machines. Theor. Comput. Sci. 375, 76–108. Extended version available as Research report BRICS RS-06-18, University of Aarhus, Dec. 2006.CrossRefGoogle Scholar
Biernacki, D., Danvy, O. & Millikin, K. (2006b, Oct.) A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations. Technical Report BRICS RS-06-15. DAIMI, Aarhus, Denmark: Department of Computer Science, University of Aarhus. Accepted for publication at TOPLAS.CrossRefGoogle Scholar
Bloo, R., Kamareddine, F. & Nederpelt, R. (1996) The Barendregt cube with definitions and generalised reduction. Inform. Comput. 126 (2), 123–143.CrossRefGoogle Scholar
Damian, D. & Danvy, O. (2003) Syntactic accidents in program analysis: On the impact of the CPS transformation. J. Funct. Programming 13 (5), 867–904. A preliminary version was presented at the 2000 ACM SIGPLAN International Conference on Functional Programming (ICFP 2000).CrossRefGoogle Scholar
Danvy, O. (1994) Back to direct style. Sci. Comput. Programming 22 (3), 183–195. A preliminary version was presented at the Fourth European Symposium on Programming (ESOP 1992).CrossRefGoogle Scholar
Danvy, O. (ed). (1997, Jan.) Proceedings of the Second ACM SIGPLAN Workshop on Continuations (CW'97). Technical report BRICS NS-96-13. Aarhus, Denmark: University of Aarhus.Google Scholar
Danvy, O. (2004) From reduction-based to reduction-free normalization. In Proceedings of the Fourth International Workshop on Reduction Strategies in Rewriting and Programming (wrs'04), Antoy, S. & Toyama, Y. (eds), Electronic Notes in Theoretical Computer Science 124 (2). Aachen, Germany: Elsevier Science, pp. 79–100. Invited talk.Google Scholar
Danvy, O. & Millikin, K. (2007) Refunctionalization at work. In Research Report BRICS RS-07-7, University of Aarhus.CrossRefGoogle Scholar
Danvy, O. & Filinski, A. (1990) Abstracting control. In Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, Wand, M. (ed), Nice, France: ACM Press, pp. 151–160.CrossRefGoogle Scholar
Danvy, O. & Filinski, A. (1992) Representing control, a study of the CPS transformation. Math. Struct. Comput. Sci. 2 (4), 361–391.CrossRefGoogle Scholar
Danvy, O. & Lawall, J. L. (1992) Back to direct style II: First-class continuations. In Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, Clinger, W. (ed), LISP Pointers, Vol. V, No. 1. San Francisco, CA: ACM Press, pp. 299–310.CrossRefGoogle Scholar
Danvy, O. & Nielsen, L. R. (2001) Defunctionalization at work. In Proceedings of the Third International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'01), Søndergaard, H. (ed.) Firenze, Italy: ACM Press, pp. 162–174. Extended version available as the technical report BRICS RS-01-23.Google Scholar
Danvy, O. & Nielsen, L. R. (2003) A first-order one-pass CPS transformation. Theor. Comput. Sci. 308 (1–3), 239–257. A preliminary version was presented at the Fifth International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002).CrossRefGoogle Scholar
Danvy, O. & Nielsen, L. R. (2004, Nov.). Refocusing in Reduction Semantics. Research Report BRICS RS-04-26. DAIMI, Aarhus, Denmark: Department of Computer Science, University of Aarhus. A preliminary version appears in the informal proceedings of the Second International Workshop on Rule-Based Programming (RULE 2001), Electronic Notes in Theoretical Computer Science 59 (4).Google Scholar
Danvy, O. & Nielsen, L. R. (2005) CPS transformation of beta-redexes. Inform. Process. Lett. 94 (5), 217–224. Extended version available as the research report BRICS RS-04-39.CrossRefGoogle Scholar
Danvy, O. & Schultz, U. P. (2000) Lambda-dropping: Transforming recursive equations into programs with block structure. Theor. Comput. Sci. 248 (1–2), 243–287.CrossRefGoogle Scholar
Danvy, O. & Talcott, C. L. (eds). (1992, June) Proceedings of the First ACM SIGPLAN Workshop on Continuations (CW'92). Technical report STAN-CS-92-1426, Stanford University.Google Scholar
deGroote, P. Groote, P. (1994) A CPS-translation of the λμ-calculus. In 19th Colloquium on Trees in Algebra and Programming (CAAP'94), Tison, S. (ed), Lecture Notes in Computer Science, No. 787. Edinburgh, Scotland: Springer-Verlag.CrossRefGoogle Scholar
Felleisen, M. (1987, Aug.) The Calculi of λ-v-cs Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. Ph.D. Thesis. Bloomington, IN: Computer Science Department, Indiana University.Google Scholar
Felleisen, M. & Flatt, M. (1989–2003) Programming Languages and Lambda Calculi. Unpublished lecture notes. Available at: http://www.ccs.neu.edu/home/matthias/3810-w02/readings.html 2006.Google Scholar
Filinski, A. (2001, Jan.) An extensional CPS transform (preliminary report). In: (Sabry 2001).Google Scholar
Fischer, M. J. (1993). Lambda-calculus schemata. Lisp Symbolic Comput. 6 (3/4), 259–288. Available at http://www.brics.dk/~hosc/vol06/03-fischer.html A preliminary version was presented at the ACM Conference on Proving Assertions about Programs, SIGPLAN Notices, Vol. 7, No. 1, January 1972.CrossRefGoogle Scholar
Flanagan, C., Sabry, A., Duba, B. F. & Felleisen, M. (1993) The essence of compiling with continuations. In Proceedings of the ACM SIGPLAN'93 Conference on Programming Languages Design and Implementation, Wall, D. W. (ed), SIGPLAN Notices, Vol. 28, No 6. Albuquerque, NM: ACM Press, pp. 237–247.Google Scholar
Fradet, P. & LeMétayer, D. Métayer, D. (1991) Compilation of functional languages by program transformation. ACM Trans. Programming Lang. Syst. 13, 21–51.CrossRefGoogle Scholar
Friedman, D. P., Wand, M. & Haynes, C. T. (2001) Essentials of Programming Languages, 2nd ed. Cambridge, MA: The MIT Press.Google Scholar
Gordon, M. J. C. (1979) The Denotational Description of Programming Languages. Springer-Verlag.CrossRefGoogle Scholar
Griffin, T. G. (1990) A formulae-as-types notion of control. In Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, Hudak, P. (ed), San Francisco, CA: ACM Press, pp. 47–58.Google Scholar
Harper, B. & Lillibridge, M. (1993) Polymorphic type assignment and CPS conversion. Lisp Symbolic Comput. 6 (3/4), 361–380. Corrigendum (2006) in Higher-Order Symbolic Comput. 16 (4): 401.CrossRefGoogle Scholar
Hatcliff, J. (1994, June) The Structure of Continuation-Passing Styles. Ph.D. Thesis, Manhattan, KS: Department of Computing and Information Sciences, Kansas State University.Google Scholar
Hatcliff, J. & Danvy, O. (1994) A generic account of continuation-passing styles. In Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, Boehm, H.-J. (ed), Portland OR: ACM Press, pp. 458–471.Google Scholar
Hatcliff, J. & Danvy, O. (1997) Thunks and the λ-calculus. J. Funct. Programming 7 (3), 303–319.CrossRefGoogle Scholar
Kelsey, R. A. (1989, May) Compilation by Program Transformation. Ph.D. Thesis. New Haven, CT: Computer Science Department, Yale University, Research Report 702.Google Scholar
Kranz, D. A. (1988, Feb.) Orbit: An Optimizing Compiler for Scheme. Ph.D. Thesis. New Haven, CT: Computer Science Department, Yale University, Research Report 632.Google Scholar
Kučan, J. (1998) Retraction approach to CPS transform. Higher-Order Symbolic Comput. 11 (2), 145–175.CrossRefGoogle Scholar
Lawall, J. L. (1994, July) Continuation Introduction and Elimination in Higher-Order Programming Languages. Ph.D. Thesis. Bloomington, IN: Computer Science Department, Indiana University.Google Scholar
Lawall, J. L. & Danvy, O. (1993) Separating stages in the continuation-passing style transformation. In Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages, Graham, S. L. (ed), Charleston, SC: ACM Press, pp. 124–136.Google Scholar
Meyer, A. R. & Wand, M. (1985) Continuation semantics in typed lambda-calculi (summary). In Logics of Programs – Proceedings, Parikh, R. (ed), Lecture Notes in Computer Science, No. 193. Brooklyn, NY: Springer-Verlag, pp. 219–224.Google Scholar
Millikin, K. (2005) A new approach to one-pass transformations. In Proceedings of the Sixth Symposium on Trends in Functional Programming (TFP 2005), vanEekelen, M. Eekelen, M. (ed), Tallinn, Estonia: Institute of Cybernetics at Tallinn Technical University, pp. 252–264. Granted the best student-paper award of TFP 2005.Google Scholar
Moggi, E. (1991) Notions of computation and monads. Inform. Comput. 93, 55–92.CrossRefGoogle Scholar
Nielsen, L. R. (2001a) A selective transformation. In Proceedings of the 17th Annual Conference on Mathematical Foundations of Programming Semantics, Brookes, S. & Mislove, M. (eds), Electronic Notes in Theoretical Computer Science, vol. 45. Aarhus, Denmark: Elsevier Science Publishers, pp. 201–222.Google Scholar
Nielsen, L. R. (2001b, July) A Study of Defunctionalization and Continuation-Passing Style. Ph.D. Thesis. Aarhus, Denmark: BRICS PhD School, University of Aarhus, BRICS DS-01-7.Google Scholar
Ohori, A. & Sasano, I. (2007) Lightweight fusion by fixed point promotion. Proceedings of the Thirty-Fourth Annual ACM Symposium on Principles of Programming Languages, Felleisen, M. (ed), Nice, France: ACM Press, pp. 143–154.Google Scholar
PeytonJones, S. L. Jones, S. L. (1987) The Implementation of Functional Programming Languages. Prentice Hall International Series in Computer Science. Prentice-Hall International.Google Scholar
Plotkin, G. D. (1975) Call-by-name, call-by-value and the λ-calculus. Theor. Comput. Sci. 1, 125–159.CrossRefGoogle Scholar
Plotkin, G. D. (1981, Sept.) A Structural Approach to Operational Semantics. Tech. Rept. FN-19. DAIMI, Aarhus, Denmark: Department of Computer Science, University of Aarhus.Google Scholar
Queinnec, C. (1996) Lisp in Small Pieces. Cambridge, England: Cambridge University Press.CrossRefGoogle Scholar
Reppy, J. (2002) Optimizing nested loops using local CPS conversion. Higher-Order Symbolic Comput. 15 (2/3), 161–180.CrossRefGoogle Scholar
Reynolds, J. C. (1972) Definitional interpreters for higher-order programming languages. In Proceedings of 25th ACM National Conference, pp. 717–740. Reprinted in Higher-Order Symbolic Comput. 11(4), 363–397, 1998, with a foreword Reynolds:HOSC98-revisited.Google Scholar
Reynolds, J. C. (1993) The discoveries of continuations. Lisp Symbolic Comput. 6 (3/4), 233–247.CrossRefGoogle Scholar
Reynolds, J. C. (1998) Definitional interpreters revisited. Higher-Order and Symbolic Comput. 11 (4), 355–361.CrossRefGoogle Scholar
Sabry, A. (1994, Aug.) The Formal Relationship Between Direct and Continuation-Passing Style Optimizing Compilers: A Synthesis of Two Paradigms. Ph.D. Thesis. Houston, TX: Computer Science Department, Rice University, Technical report 94-242.Google Scholar
Sabry, A. (ed). (2001, Jan.) Proceedings of the Third ACM SIGPLAN Workshop on Continuations (cw'01). Technical report 545, Computer Science Department, Indiana University.Google Scholar
Sabry, A. & Felleisen, M. (1993) Reasoning about programs in continu-ation-passing style. Lisp Symbolic Comput. 6 (3/4), 289–360.CrossRefGoogle Scholar
Sabry, A. & Felleisen, M. (1994) Is continuation-passing useful for data flow analysis? In Proceedings of the ACM SIGPLAN'94 Conference on Programming Languages Design and Implementation, Sarkar, V. (ed.), SIGPLAN Notices, Vol. 29, No 6. Orlando, FL: ACM Press, pp. 1–12.Google Scholar
Sabry, A. & Wadler, P. (1997) A reflection on call-by-value. ACM Trans. Programming Lang. Sys. 19 (6), 916–941. A preliminary version was presented at the 1996 ACM SIGPLAN International Conference on Functional Programming (ICFP 1996).CrossRefGoogle Scholar
Shan, C.-C. (2004, Sept.) Shift to control. In Proceedings of the 2004 ACM SIGPLAN Workshop on Scheme and Functional Programming, Shivers, O. & Waddell, O. (eds), Technical Report TR600, Computer Science Department, Indiana University.Google Scholar
Shan, C.-C. (2007) A static simulation of dynamic delimited control. Higher-Order Symbolic Comput. 20 (4), Journal version of (Shan 2004).CrossRefGoogle Scholar
Shivers, O. 1991 (May) Control-Flow Analysis of Higher-Order Languages or Taming Lambda. Ph.D. Thesis. Pittsburgh, PA: School of Computer Science, Carnegie Mellon University, Technical Report CMU-CS-91-145.Google Scholar
Steele, G. L. (1978, May) Rabbit: A Compiler for Scheme. M.Sc. thesis. Cambridge: Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Technical Report AI-TR-474.Google Scholar
Strachey, C. & Wadsworth, C. P. (1974) Continuations: A Mathematical Semantics for Handling Full Jumps. Technical Monograph PRG-11. Oxford, England: Oxford University Computing Laboratory, Programming Research Group. Reprinted in Higher-Order Symbolic Comput. 13 (1/2), 135–152, 2000, with a foreword (Reynolds 1998).Google Scholar
Thielecke, H. (1997) Categorical Structure of Continuation Passing Style. Ph.D. thesis. Edinburgh, Scotland: University of Edinburgh, ECS-LFCS-97-376.Google Scholar
Thielecke, H. (ed). (2004, Jan.) Proceedings of the Fourth ACM SIGPLAN Workshop on Continuations (cw'04). Technical report CSR-04-1, Department of Computer Science, Queen Mary's College.Google Scholar
Wadsworth, C. P. (2000) Continuations revisited. Higher-Order Symbolic Comput 13 (1/2), 131–133.CrossRefGoogle Scholar
Wand, M. (1991) Correctness of procedure representations in higher-order assembly language. In Proceedings of the 7th International Conference on Mathematical Foundations of Programming Semantics, Brookes, S., Main, M., Melton, A., Mislove, M. & Schmidt, D. (eds), Lecture Notes in Computer Science, No. 598. Pittsburgh, PA: Springer-Verlag, pp. 294–311.Google Scholar
Xiao, Y., Sabry, A. & Ariola, Z. M. (2001) From syntactic theories to interpreters: Automating proofs of unique decomposition. Higher-Order and Symbolic Comput. 14 (4), 387–409.CrossRefGoogle Scholar
Zdancewic, S. & Myers, A. (2002) Secure information flow via linear continuations. Higher-Order Symbolic Comput. 15 (2/3), 209–234.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.