More Web Proxy on the site http://driver.im/

Article

A First-Order One-Pass CPS Transformation

Authors:

Lasse R. NielsenAuthors Info & Claims

FoSSaCS '02: Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures

Pages 98 - 113

Published: 08 April 2002 Publication History

Abstract

We present a new transformation of call-by-value lambda-terms into continuation-passing style (CPS). This transformation operates in one pass and is both compositional and first-order. Because it operates in one pass, it directly yields compact CPS programs that are comparable to what one would write by hand. Because it is compositional, it allows proofs by structural induction. Because it is first-order, reasoning about it does not require the use of a logical relation.This new CPS transformation connects two separate lines of research. It has already been used to state a new and simpler correctness proof of a direct-style transformation, and to develop a new and simpler CPS transformation of control-flow information.

References

[1]

Andrew W. Appel. Compiling with Continuations . Cambridge University Press, New York, 1992.

[2]

Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics , volume 103 of Studies in Logic and the Foundation of Mathematics . North-Holland, 1984. Revised edition.

[3]

William D. Clinger. Proper tail recursion and space efficiency. In Keith D. Cooper, editor, Proceedings of the ACM SIGPLAN'98 Conference on Programming Languages Design and Implementation , pages 174-185, Montréal, Canada, June 1998. ACM Press.

[4]

Daniel Damian. On Static and Dynamic Control-Flow Information in Program Analysis and Transformation . PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, July 2001. BRICS DS-01-5.

[5]

Daniel Damian and Olivier Danvy. A simple CPS transformation of control-flow information. Technical Report BRICS RS-01-55, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 2001.

[6]

Daniel Damian and Olivier Danvy. Syntactic accidents in program analysis: On the impact of the CPS transformation. Journal of Functional Programming , 2002. To appear. Extended version available as the technical report BRICS-RS-01-54.

[7]

Olivier Danvy. Back to direct style. Science of Computer Programming , 22(3):183- 195, 1994.

[8]

Olivier Danvy. Formalizing implementation strategies for first-class continuations. In Gert Smolka, editor, Proceedings of the Ninth European Symposium on Programming , number 1782 in Lecture Notes in Computer Science, pages 88-103, Berlin, Germany, March 2000. Springer-Verlag.

[9]

Olivier Danvy, Belmina Dzafic, and Frank Pfenning. On proving syntactic properties of CPS programs. In Third International Workshop on Higher-Order Operational Techniques in Semantics , volume 26 of Electronic Notes in Theoretical Computer Science , pages 19-31, Paris, France, September 1999. Also available as the technical report BRICS RS-99-23.

[10]

Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science , 2(4):361-391, 1992.

[11]

Olivier Danvy and Lasse R. Nielsen. CPS transformation of beta-redexes. In Amr Sabry, editor, Proceedings of the Third ACM SIGPLAN Workshop on Continuations , Technical report 545, Computer Science Department, Indiana University, pages 35-39, London, England, January 2001. Also available as the technical report BRICS RS-00-35.

[12]

Olivier Danvy and Lasse R. Nielsen. Defunctionalization at work. In Harald Søndergaard, editor, Proceedings of the third International Conference on Principles and Practice of Declarative Programming , pages 162-174, Firenze, Italy, September 2001. ACM Press. Extended version available as the technical report BRICS RS-01-23.

[13]

Olivier Danvy and Lasse R. Nielsen. A first-order one-pass CPS transformation. Technical Report BRICS RS-01-49, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 2001. Extended version of an article to appear in the proceedings of FOSSACS'02, Grenoble, France, April 2002.

[14]

Olivier Danvy and Lasse R. Nielsen. A higher-order colon translation. In Kuchen and Ueda {23}, pages 78-91. Extended version available as the technical report BRICS RS-00-33.

[15]

Olivier Danvy and Lasse R. Nielsen. Syntactic theories in practice. In Mark van den Brand and Rakesh M. Verma, editors, Informal proceedings of the Second International Workshop on Rule-Based Programming (RULE 2001) , volume 59.4 of Electronic Notes in Theoretical Computer Science , Firenze, Italy, September 2001. Extended version available as the technical report BRICS RS-01-31.

[16]

Olivier Danvy and Frank Pfenning. The occurrence of continuation parameters in CPS terms. Technical report CMU-CS-95-121, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, February 1995.

[17]

Belmina Dzafic. Formalizing program transformations. Master's thesis, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 1998.

[18]

Daniel P. Friedman, Mitchell Wand, and Christopher T. Haynes. Essentials of Programming Languages . The MIt Press and McGraw-Hill, 1991.

[19]

Daniel P. Friedman, Mitchell Wand, and Christopher T. Haynes. Essentials of Programming Languages, second edition . the MIT Press, 2001.

[20]

Timothy G. Griffin. A formulae-as-types notion of control. In Paul Hudak, editor, Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages , pages 47-58, San Francisco, California, January 1990. ACM Press.

[21]

John Hatcliff and Olivier Danvy. A generic account of continuation-passing styles. In Hans-J. Boehm, editor, Proceedings of the twenty-First Annual ACM Symposium on Principles of Programming Languages , pages 458-471, Portland, Oregon, January 1994. ACM Press.

[22]

David Kranz, Richard Kesley, Jonathan Rees, Paul Hudak, Jonathan Philbin, and Norman Adams. Orbit: An optimizing compiler for Scheme. In Proceedings of the ACM SIGPLAN'86 Symposium on Compiler Construction , pages 219-233, Palo Alto, California, June 1986. ACM Press.

[23]

Herbert Kuchen and Kazunori Ueda, editors. Functional and Logic Programming, 5th International Symposium, FLOPS 2001 , number 2024 in Lecture Notes in Computer Science, tokyo, Japan, March 2001. Springer-Verlag.

[24]

Albert R. Meyer and Mitchell Wand. Continuation semantics in typed lambda-calculi (summary). In Rohit Parikh, editor, Logics of Programs - Proceedings , number 193 in Lecture Notes in Computer Science, pages 219-224, Brooklyn, June 1985. Springer-Verlag.

[25]

Eugenio Moggi. Notions of computation and monads. Information and Computation , 93:55-92, 1991.

[26]

Chetan R. Murthy. Extracting Constructive Content from Classical Proofs . PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, 1990.

[27]

Lasse R. Nielsen. A study of defunctionalization and continuation-passing style . PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, July 2001. BRICS DS-01-7.

[28]

Lasse R. Nielsen. A simple correctness proof of the direct-style transformation. Technical Report BRICS RS-02-02, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, January 2002.

[29]

Jens Palsberg and Mitchell Wand. CPS transformation of flow information. Unpublished manuscript, available at http://www.cs.purdue.edu/~palsberg/publications.html, June 2001.

[30]

Gordon D. Plotkin. Call-by-name, call-by-value and The ¿-calculus. Theoretical Computer Science , 1:125-159, 1975.

[31]

Jeff Polakow. Ordered Linear Logic and Applications . PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, August 2001. Technical Report CMU-CS-01-152.

[32]

Jeff Polakow and Frank Pfenning. Natural deduction for intuitionistic noncommutative linear logic. In Jean-Yves Girard, editor, Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications , number 1581 in Lecture Notes in Computer Science, pages 295-309, L'Aquila, Italy, April 1999. Springer-Verlag.

[33]

Jeff Polakow and Frank Pfenning. Properties of terms in continuation passing style in an ordered logical framework. In Joëlle Despeyroux, editor, Workshop on Logical Frameworks and Meta-Languages (LFM 2000) , Santa Barbara, California, June 2000. http://www-sop.inria.fr/certilab/LFM00/Proceedings/.

[34]

Jeff Polakow and Kwangkeun Yi. Proving syntactic properties of exceptions in an ordered logical framework. In Kuchen and Ueda {23}, pages 61-77.

[35]

John C. Reynolds. The discoveries of continuations. Lisp and Symbolic Computation , 6(3/4):233-247, 1993.

[36]

John C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation , 11(4):363-397, 1998. Reprinted from the proceedings of the 25th ACM National Conference (1972).

[37]

Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation , 6(3/4):289-360, 1993.

[38]

Amr Sabry and Philip Wadler. A reflection on call-by-value. ACM transactions on Programming Languages and Systems , 19(6):916-941, 1997.

[39]

Guy L. Steele Jr. Rabbit: A compiler for Scheme. technical Report AI-tR-474, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, May 1978.

[40]

Mitchell Wand. Embedding type structure in semantics. In Mary S. Van Deusen and Zvi Galil, editors, Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages , pages 1-6, New Orleans, Louisiana, January 1985. ACM Press.

[41]

Mitchell Wand. Correctness of procedure representations in higher-order assembly language. In Stephen Brookes, Michael Main, Austin Melton, Michael Mislove, and David Schmidt, editors, Mathematical Foundations of Programming Semantics , number 598 in Lecture Notes in Computer Science, pages 294-311, Pittsburgh, Pennsylvania, March 1991. Springer-Verlag. 7th International Conference.

[42]

Glynn Winskel. The Formal Semantics of Programming Languages . Foundation of Computing Series. the MIT Press, 1993.

Cited By

Lindley SMorris J(2016)Talking bananas: structural recursion for session typesACM SIGPLAN Notices10.1145/3022670.295192151:9(434-447)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/3022670.2951921
Lindley SMorris JGarrigue JKeller GSumii E(2016)Talking bananas: structural recursion for session typesProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming10.1145/2951913.2951921(434-447)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/2951913.2951921
Tian Y(2006)Mechanically verifying correctness of CPS compilationProceedings of the Twelfth Computing: The Australasian Theory Symposium - Volume 5110.5555/2523791.2523799(41-51)Online publication date: 16-Jan-2006
https://dl.acm.org/doi/10.5555/2523791.2523799
Show More Cited By

A First-Order One-Pass CPS Transformation
1. Theory of computation

Recommendations

A first-order one-pass CPS transformation

We present a new transformation of λ-terms into continuation-passing style (CPS). This transformation operates in one pass and is both compositional and first-order. Previous CPS transformations only enjoyed two out of the three properties of being ...
On one-pass CPS transformations

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 ...
Proving Isomorphism of First-Order Logic Proof Systems in HOL

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FoSSaCS '02: Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures

April 2002

435 pages

ISBN:354043366X

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 08 April 2002

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lindley SMorris J(2016)Talking bananas: structural recursion for session typesACM SIGPLAN Notices10.1145/3022670.295192151:9(434-447)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/3022670.2951921
Lindley SMorris JGarrigue JKeller GSumii E(2016)Talking bananas: structural recursion for session typesProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming10.1145/2951913.2951921(434-447)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/2951913.2951921
Tian Y(2006)Mechanically verifying correctness of CPS compilationProceedings of the Twelfth Computing: The Australasian Theory Symposium - Volume 5110.5555/2523791.2523799(41-51)Online publication date: 16-Jan-2006
https://dl.acm.org/doi/10.5555/2523791.2523799
Tian Y(2006)Mechanically verifying correctness of CPS compilationProceedings of the 12th Computing: The Australasian Theroy Symposium - Volume 5110.5555/1151785.1151791(41-51)Online publication date: 1-Jan-2006
https://dl.acm.org/doi/10.5555/1151785.1151791
Danvy O(2003)A new one-pass transformation into monadic normal formProceedings of the 12th international conference on Compiler construction10.5555/1765931.1765939(77-89)Online publication date: 7-Apr-2003
https://dl.acm.org/doi/10.5555/1765931.1765939
Minamide YOkuma K(2003)Verifying CPS transformations in Isabelle/HOLProceedings of the 2003 ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding10.1145/976571.976576(1-8)Online publication date: 26-Aug-2003
https://dl.acm.org/doi/10.1145/976571.976576
Kameyama YHasegawa M(2003)A sound and complete axiomatization of delimited continuationsACM SIGPLAN Notices10.1145/944746.94472238:9(177-188)Online publication date: 25-Aug-2003
https://dl.acm.org/doi/10.1145/944746.944722
Kameyama YHasegawa MRunciman CShivers O(2003)A sound and complete axiomatization of delimited continuationsProceedings of the eighth ACM SIGPLAN international conference on Functional programming10.1145/944705.944722(177-188)Online publication date: 25-Aug-2003
https://dl.acm.org/doi/10.1145/944705.944722
Thielecke H(2003)From control effects to typed continuation passingACM SIGPLAN Notices10.1145/640128.60414438:1(139-149)Online publication date: 15-Jan-2003
https://dl.acm.org/doi/10.1145/640128.604144
Thielecke HAiken AMorrisett G(2003)From control effects to typed continuation passingProceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/604131.604144(139-149)Online publication date: 15-Jan-2003
https://dl.acm.org/doi/10.1145/604131.604144

View Options

View options

Media

Figures

Other

Tables

View Table of Contents