×

zbMATH — the first resource for mathematics

Representing control: A study of the CPS transformation. (English) Zbl 0798.68102
Summary: This paper investigates the transformation of \(\lambda_ v\)-terms into continuation-passing style (CPS). We show that by appropriate \(\eta\)- expansion of Fischer and Plotkin’s two-pass equational specification of the CPS transform, we can obtain a static and context-free separation of the result terms into “essential” and “administrative” constructs. Interpreting the former as syntax builders and the latter as directly executable code, we obtain a simple and efficient one-pass transformation algorithm, easily extended to conditional expressions, recursive definitions, and similar constructs. This new transformation algorithm leads to a simpler proof of Plotkin’s simulation and indifference results.
We go on to show how CPS-based control operators similar to, but more general than, Scheme’s call/cc can be naturally accommodated by the new transformation algorithm. To demonstrate the expressive power of these operators, we use them to present an equivalent but even more concise formulation of the efficient CPS transformation algorithm. Finally, we relate the fundamental ideas underlying this derivation to similar concepts from other work on program manipulation; we derive a one-pass CPS transformation of \(\lambda_ n\)-terms; and we outline some promising area for future research.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B40 Combinatory logic and lambda calculus
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] DOI: 10.1145/91556.91622 · doi:10.1145/91556.91622
[2] Danvy, Proceedings of the 1992 ACM Conference on Lisp and Functional Programming (1992)
[3] Danvy, Proceedings of the Fourth European Symposium on Programming 582 pp 130– (1992)
[4] Danvy, Special issue of the BIGRE journal: Putting Scheme to Work 65 pp 10– (1989)
[5] Wadler, Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages pp 1– (1992)
[6] Consel, Proceedings of the Fifth ACM Conference on Functional Programming and Computer Architecture 523 pp 496– (1991)
[7] Steele, Rabbit: A Compiler for Scheme (1978)
[8] Consel, Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming Languages pp 14– (1991)
[9] DOI: 10.1145/382130.382133 · doi:10.1145/382130.382133
[10] DOI: 10.1145/91556.91626 · doi:10.1145/91556.91626
[11] DOI: 10.1145/800055.802052 · doi:10.1145/800055.802052
[12] Shivers, SIGPLAN Notices 26 pp 190– (1991)
[13] DOI: 10.1016/0167-6423(91)90002-F · Zbl 0745.68073 · doi:10.1016/0167-6423(91)90002-F
[14] Sabry, Proceedings of the 1992 ACM Conference on Lisp and Functional Programming (1922)
[15] DOI: 10.1016/0167-6423(91)90035-V · Zbl 0745.68039 · doi:10.1016/0167-6423(91)90035-V
[16] Appel, Compiling with Continuations (1992)
[17] Reynolds, Proceedings of 25th ACM National Conference pp 717– (1972)
[18] DOI: 10.1016/0304-3975(75)90017-1 · Zbl 0325.68006 · doi:10.1016/0304-3975(75)90017-1
[19] DOI: 10.1016/0304-3975(86)90006-X · Zbl 0632.68007 · doi:10.1016/0304-3975(86)90006-X
[20] DOI: 10.1016/0304-3975(89)90091-1 · Zbl 0696.68093 · doi:10.1016/0304-3975(89)90091-1
[21] Murthy, Proceedings of the ACM SIGPLAN Work-shop on Continuations (1992)
[22] DOI: 10.1109/LICS.1989.39155 · doi:10.1109/LICS.1989.39155
[23] Milner, The definition of standard ML. (1990)
[24] Mellish, Implements of PROLOG pp 147– (1984)
[25] DOI: 10.1007/BF01806312 · doi:10.1007/BF01806312
[26] Harber, Proceedings of the ACM SIGPLAN Workshop on Continuations (1992)
[27] Griffin, The Icon Programming Language (1983)
[28] Griffin, Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages pp 47– (1990)
[29] DOI: 10.1145/114005.102805 · doi:10.1145/114005.102805
[30] DOI: 10.1145/942578.807077 · doi:10.1145/942578.807077
[31] Fillnski, Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages pp 27– (1992)
[32] DOI: 10.1145/62678.62684 · doi:10.1145/62678.62684
[33] DOI: 10.1016/0304-3975(87)90109-5 · Zbl 0643.03011 · doi:10.1016/0304-3975(87)90109-5
[34] Felleisen, Proceedings of the First Symposium on Logic in Computer Science pp 131– (1986)
[35] Felleisen, Beyond continuations 216 (1987)
[36] Felleisen, Proceedings of the Fifteenth Annual ACM Symposium on Principles of Programming Languages pp 180– (1988)
[37] Duba, Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming Languages pp 163– (1991)
[38] Wand, Mathematical Foundations of Programming Semantics 598 pp 294– (1991) · doi:10.1007/3-540-55511-0_15
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.