Formalizing Implementation Strategies for First-Class Continuations

  • Olivier Danvy
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1782)


We present the first formalization of implementation strategies for first-class continuations. The formalization hinges on abstract machines for continuation-passing style (CPS) programs with a special treatment for the current continuation, accounting for the essence of first-class continuations. These abstract machines are proven equivalent to a standard, substitution-based abstract machine. The proof techniques work uniformly for various representations of continuations. As a byproduct, we also present a formal proof of the two folklore theorems that one continuation identifier is enough for second-class continuations and that second-class continuations are stackable.

A large body of work exists on implementing continuations, but it is predominantly empirical and implementation-oriented. In contrast, our formalization abstracts the essence of first-class continuations and provides a uniform setting for specifying and formalizing their representation.


Abstract Machine Standard Machine Program Language Design Direct Style Tail Call 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Andrew W. Appel and David B. MacQueen. Standard ML of New Jersey. In Third International Symposium on Programming Language Implementation and Logic Programming, number 528 in Lecture Notes in Computer Science, pages 1–13, Passau, Germany, August 1991.Google Scholar
  2. 2.
    David B. Bartley and John C. Jensen. The implementation of PC Scheme. In Proceedings of the 1986 ACM Conference on Lisp and Functional Programming, pages 86–93, Cambridge, Massachusetts, August 1986.Google Scholar
  3. 3.
    Daniel M. Berry. Block structure: Retention or deletion? (extended abstract). In Conference Record of the Third Annual ACM Symposium on Theory of Computing, pages 86–100, Shaker Heights, Ohio, May 1971.Google Scholar
  4. 4.
    William Clinger, Anne H. Hartheimer, and Eric M. Ost. Implementation strategies for first-class continuations. Higher-Order and Symbolic Computation, 12(1):7–45, 1999.zbMATHCrossRefGoogle Scholar
  5. 5.
    Olivier Danvy. Memory allocation and higher-order functions. In Proceedings of the ACM SIGPLAN’87 Symposium on Interpreters and Interpretive Techniques, SIGPLAN Notices, Vol. 22, No 7, pages 241–252, Saint-Paul, Minnesota, June 1987.CrossRefGoogle Scholar
  6. 6.
    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.Google Scholar
  7. 7.
    Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361–391, 1992.zbMATHMathSciNetCrossRefGoogle Scholar
  8. 8.
    Olivier Danvy and Julia L. Lawall. Back to direct style II: First-class continuations. In Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, LISP Pointers, Vol. V, No. 1, pages 299–310, San Francisco, California, June 1992.CrossRefGoogle Scholar
  9. 9.
    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.Google Scholar
  10. 10.
    Bruce F. Duba, Robert Harper, and David B. MacQueen. Typing first-class continuations in ML. In Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, pages 163–173, Orlando, Florida, January 1991.Google Scholar
  11. 11.
    Belmina Dzafic. Formalizing program transformations. Master’s thesis, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 1998.Google Scholar
  12. 12.
    Matthias Felleisen. The Calculi of λ-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Department of Computer Science, Indiana University, Bloomington, Indiana, August 1987.Google Scholar
  13. 13.
    Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In Proceedings of the ACM SIGPLAN’93 Conference on Programming Languages Design and Implementation, SIGPLAN Notices, Vol. 28, No 6, pages 237–247, Albuquerque, New Mexico, June 1993.Google Scholar
  14. 14.
    Christopher T. Haynes and Daniel P. Friedman. Embedding continuations in procedural objects. ACM Transactions on Programming Languages and Systems, 9(4):582–598, 1987.zbMATHCrossRefGoogle Scholar
  15. 15.
    Robert Hieb, R. Kent Dybvig, and Carl Bruggeman. Representing control in the presence of first-class continuations. In Proceedings of the ACM SIGPLAN’90 Conference on Programming Languages Design and Implementation, SIGPLAN Notices, Vol. 25, No 6, pages 66–77, White Plains, New York, June 1990.Google Scholar
  16. 16.
    Richard A. Kelsey and Jonathan A. Rees. A tractable Scheme implementation. Lisp and Symbolic Computation, 7(4):315–336, 1994.CrossRefGoogle Scholar
  17. 17.
    David Kranz, Richard Kesley, Jonathan Rees, Paul Hudak, Jonathan Philbin, and Norman Adams. Orbit: An optimizing compiler for Scheme. In Proceedings of the 1986 Symposium on Compiler Construction, SIGPLAN Notices, Vol. 21, No 7, pages 219–233, Palo Alto, California, June 1986.CrossRefGoogle Scholar
  18. 18.
    Peter J. Landin. The mechanical evaluation of expressions. Computer Journal, 6:308–320, 1964.zbMATHGoogle Scholar
  19. 19.
    Drew McDermott. An efficient environment allocation scheme in an interpreter for a lexically-scoped Lisp. In Conference Record of the 1980 LISP Conference, pages 154–162, Stanford, California, August 1980.Google Scholar
  20. 20.
    Gordon D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125–159, 1975.zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    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.Google Scholar
  22. 22.
    Christopher Strachey and Christopher P. Wadsworth. Continuations: A mathematical semantics for handling full jumps. Higher-Order and Symbolic Computation, 13(1/2), 2000. Reprint of the technical monograph PRG-11, Oxford University Computing Laboratory (1974).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Olivier Danvy
    • 1
  1. 1.BRICS, Department of Computer ScienceUniversity of AarhusAarhus CDenmark

Personalised recommendations