Amr Sabry
Matthias Felleisen
Abstract
Plotkin's λ-value calculus is sound but incomplete for reasoning about β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 β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 βη can prove the corresponding equation between CPS programs. The extended calculus is equivalent to an untyped variant of Moggi's computational λ-calculus.
- 1 APPEL, A. AND T. JIM. Continuation-passing, closure-passing style. In Proc. 16th A aM Sympos,um on Principles of Programming Languages, 1982, 293-302. Google Scholar
Digital Library
- 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.Google Scholar
- 3 DANVY, O. Back to direct style. In 4th Proc. European Symposium on Programming. Springer Lecture Notes in Computer Science, 582. Springer Verlag, Berlin, 1992, 130-150. Google ScholarDigital Library
- 4 DANVY, O. Three steps for the CPS transformation. Tech. Rep. CIS-92-2. Kansas State University, 1992.Google Scholar
- 5 DANVY, O. AND A. FILINSKI. Representing control: A study of the CPS transformation. Tech. Rpt. CIS-91-2. Kansas State University, 1991.Google Scholar
- 6 DANVY, O. AND J. LAWALL. Back to direct style II: First-class continuations. In Proc. 1992 A CM Conference on Lisp and Functional Programming, 1992, this volume. Google ScholarDigital Library
- 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.Google Scholar
- 8 FELLEISEN, M. AND R. HIEB. The revised report on the syntactic theories of sequential control and state. Technical l~eport 100, Rice University, June 1989. Theor. Comput. Sci., 1991, to appear. Google ScholarDigital Library
- 9 FELLEISEN, M., I). FRIEDMAN, E. KOHLBECKER, AND B. DUBA. A syntactic theory of sequential control. Theor. Comput. Sci. 52(3), 1987, 205- 237. Preliminary version in: Proc. Symposium on Logic in Computer Science, 1986, 131-141. Google ScholarDigital Library
- 10 FISCHER, M.J. Lambda calculus schemata. In Proc. A CM Conference on Proving Assertions About Programs, $IGPLAN Notices 7(1), 1972, 104-109. Google ScholarDigital Library
- 11 GATELEY~ J. AND B.F. DUBA. Call-by-valuecombinatory logic and the lambda-valuc calculus. In Proc. 1991 Workshop on Mathematical Foundations of Programming Semantics. Lecture Notes in Computer Science 517, to appear. Google ScholarDigital Library
- 12 HIEB R., P~. K. DYBVIG, AND C. BRUGGEMAN. Representing control in the presence of first-class continuations. In Proceedings of the SIGPLAN '90 Conference on Programming Language Design and Implementation, June 1990, 66-77. Google ScholarDigital Library
- 13 KRANZ, D., et al. ORBIT: An optimizing compiler for Scheme. In Proc. $IGPLAN 1986 Symposium on Compiler Construction, SIGPLAN Notices 21(7), 1986, 219-233. Google ScholarDigital Library
- 14 LANDIN, P.J. The mechanical evaluation of expressions. Comput. J. 6(4), 1964, 308-320.Google ScholarCross Ref
- 15 LEaOY, X. The Zinc experiement. Technical Report 117. iNRIA, 1990.Google Scholar
- 16 MOGGI, E. Computational lambda-calculus and monads. In Proc. Symposium on Logic ~n Computer Science, 1989, 14-23. Also appeared as: LFCS Report ECS-LFCS-88-66, University of Edinburgh, 1988. Google ScholarDigital Library
- 17 PLOTKIN, G.D. Call-by-name, call-by-value, and the A-calculus. Theor. Comput. Sci. 1, 1975, 125- 159.Google ScholarCross Ref
- 18 REYNOLDS, J.C. Definitional interpreters for higher-order programming languages. In Proc. A CM Annual Conference, 1972, 717-740. Google ScholarDigital Library
- 19 SHIVERS, O. Control-flow Analysis of Higher-Order Languages or Taming Lambda. Ph.D. dissertation, Carnegie-Mellon University, t991. Google ScholarDigital Library
- 20 STEELE, G.L., Ja. RABBIT: A compiler for SCHEME. Memo 474, MIT AI Lab, 1978. Google ScholarDigital Library
Index Terms
- Reasoning about programs in continuation-passing style.
Recommendations
A generic account of continuation-passing styles
POPL '94: Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe 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 ...
Reasoning about programs in continuation-passing style.
LFP '92: Proceedings of the 1992 ACM conference on LISP and functional programmingPlotkin's λ-value calculus is sound but incomplete for reasoning about β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-...
Proofs, tests and continuation passing style
The concept of syntactical duality is central in logic. In particular, the duality defined by classical negation, or more syntactically by left and right in sequents, has been widely used to relate logic and computations. We study the proof/test duality ...
Comments