# Sharing Continuations: Proofnets for Languages with Explicit Control

## Abstract

We introduce graph reduction technology that implements functional languages with control, such as Scheme with call/cc, where continuations can be manipulated explicitly as values, and can be optimally reduced in the sense of Lévy. The technology is founded on *proofnets* for multiplicative-exponential linear logic, extending the techniques originally proposed by Lamping, where we adapt the continuation-passing style transformation to yield a new understanding of sharable values. Confluence is maintained by returning multiple answers to a (shared) continuation.

*Proofnets* provide a *concurrent* version of linear logic proofs, eliminating structurally irrelevant sequentialization, and ignoring asymmetric distinctions between inputs and outputs—dually, expressions and continuations. While Lamping’s graphs and their variants encode an embedding of intuitionistic logic into linear logic, our construction implicitly contains an embedding of classical logic into linear logic.

We propose a family of translations, produced uniformly by beginning with a continuation-passing style semantics for the languages, employing standard codings into proofnets using call-by-value, call-by-name—or hybrids of the two—to locate proofnet *boxes*, and converting the proofnets to direct style. The resulting graphs can be reduced simply (cut elimination for linear logic), have a consistent semantics that is preserved by reduction (geometry of interaction, via the so-called *context semantics*), and allow shared, incremental evaluation of continuations (optimal reduction).

## Keywords

Control Operator Classical Logic Intuitionistic Logic Linear Logic Graph Reduction## References

- 1.A. Asperti.
*δo*!*∈*= 1: Optimizing optimal*λ*-calculus implementations. In*Rewriting Techniques and Applications*, pages 102–116, Kaiserslautern, Germany, 1995.Google Scholar - 2.A. Asperti and C. Laneve. Paths, computations and labels in the lambda-calculus. In
*Rewriting Techniques and Applications, 5th International Conference*, volume 690, pages 152–167. Lecture Notes in Computer Science, 1993.Google Scholar - 3.A. Bawden. Implementing distributed systems using linear naming. TR 1627, MIT AI Lab, March 1993. (PhD thesis, originally titled
*Linear Graph Reduction: Confronting the Cost of Naming*. MIT, May 1992).Google Scholar - 4.C. Bruggeman, O. Waddell, and R.K. Dybvig. Representing control in the presence of one-shot continuations. In
*Proceedings of the ACM SIGPLAN’96 Conference on Programming Language Design and Implementation*, volume 31(5), pages 99–107, Philadephia, Pennsylvania, May 1996. SIGPLAN Notices.Google Scholar - 5.O. Danvy. Back to direct style.
*Science of Computer Programming*, 22(3):183–195, 1994.zbMATHCrossRefMathSciNetGoogle Scholar - 6.O. Danvy and A. Filinski. Abstracting control. In
*Proceeding of the 1990 ACM Conference on Lisp and Functional Programming*, pages 151–160, Nice, France, June 1990. ACM Press.Google Scholar - 7.O. Danvy and A. Filinski. Representing control: A study of the CPS transformation.
*Mathematical Structures in Computer Science*, 4:361–391, 1992.MathSciNetCrossRefGoogle Scholar - 8.A. Filinski. Declarative continuations and categorical duality. Technical Report 89/11, University of Copenhagen, 1989. Masters Thesis.Google Scholar
- 9.A. Filinski. Linear continuations. In
*Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, pages 27–38, Albuquerque, New Mexico, January 1992.Google Scholar - 10.A. Filinski. Representing monads. In
*Conference Record of POPL’ 94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, pages 446–457, Portland, Oregon, January 1994.Google Scholar - 11.J.-Y. Girard. Linear logic.
*Theoretical Computer Science*, 46:1–102, 1986.CrossRefMathSciNetGoogle Scholar - 12.G. Gonthier, M. Abadi, and J.-J. Lévy. The geometry of optimal lambda reduction. In
*Conference record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, pages 15–26, Albuquerque, New Mexico, January 1992.Google Scholar - 13.G. Gonthier, M. Abadi, and J.-J. Lévy. Linear logic without boxes. In
*Proceedings of the Seventh Annual Symposium on Logic in Computer Science*, pages 223–234, June 1992.Google Scholar - 14.T. Griffin. A formulae-as-types notion of control. In
*Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages*, pages 47–58, San Francisco, California, January 1990.Google Scholar - 15.J. Hatcliff and O. Danvy. A generic account of continuation-passing styles. In
*Conference Record of POPL’ 94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, pages 458–471, Portland, Oregon, January 1994.Google Scholar - 16.R. Hieb, R.K. Dybvig, and C. Bruggeman. Representing control in the presence of first-class continuations. In
*Proceedings of the ACM SIGPLAN’90 Conference on Programming Language Design and Implementation*, volume 25(6), pages 66–77, White Plains, New York, June 1990. SIGPLAN Notices.Google Scholar - 17.J. Lamping. An algorithm for optimal lambda calculus reduction. In
*Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages*, pages 16–30, San Francisco, California, January 1990.Google Scholar - 18.J.-J. Lévy.
*Optimal Reductions in the Lambda-Calculus*, pages 159–191. Academic Press, 1980.Google Scholar - 19.I. Mackie.
*The Geometry of Implementation*. PhD thesis, University of London, September 1994.Google Scholar - 20.I. Mackie. YALE: Yet another lambda evaluator based on interaction nets. In
*Proceedings of the ACM SIGPLAN International Conference on Functional Programming*, pages 117–128, Baltimore, Maryland, September 1998.Google Scholar - 21.C.R. Murthy.
*Extracting Constructive Content from Classical Proofs*. PhD thesis, Cornell University, August 1990.Google Scholar - 22.S. Nishizaki. Programs with continuations and linear logic.
*Science of Computer Programming*, 21(2):165–190, 1993.zbMATHCrossRefMathSciNetGoogle Scholar - 23.M. Parigot. Lambda-mu-calculus: an algorithmic interpretation of classical natural deduction. In A. Voronkov, editor,
*Logic Programming and Automated Reasoning: International Conference LPAR’ 92 Proceedings, St. Petersburg, Russia*, pages 190–201, Berlin, DE, 1992. Springer-Verlag.Google Scholar - 24.G. D. Plotkin. Call-by-name, call-by-value and the lambda calculus.
*Theoretical Computer Science*, 1:125–159, 1975.zbMATHCrossRefMathSciNetGoogle Scholar - 25.A. Sabry and M. Felleisen. Reasoning about programs in continuation-passing style.
*Lisp and Symbolic Computation*, 6(3/4):289–360, November 1993.CrossRefGoogle Scholar - 26.H. Schellinx.
*The Noble Art of Linear Decorating*. PhD thesis, Institute for Logic, Language and Computation, University of Amsterdam, 1994.Google Scholar - 27.D. Sitaram and M. Felleisen. Control delimiters and their hierarchies.
*Lisp and Symbolic Computation*, 3(1):67–99, January 1990CrossRefGoogle Scholar