Advertisement

Sharing Continuations: Proofnets for Languages with Explicit Control

  • Julia L. Lawall
  • Harry G. Mairson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1782)

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 
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.

References

  1. 1.
    A. Asperti. δo! = 1: Optimizing optimal λ-calculus implementations. In Rewriting Techniques and Applications, pages 102–116, Kaiserslautern, Germany, 1995.Google Scholar
  2. 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. 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. 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. 5.
    O. Danvy. Back to direct style. Science of Computer Programming, 22(3):183–195, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 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. 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. 8.
    A. Filinski. Declarative continuations and categorical duality. Technical Report 89/11, University of Copenhagen, 1989. Masters Thesis.Google Scholar
  9. 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. 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. 11.
    J.-Y. Girard. Linear logic. Theoretical Computer Science, 46:1–102, 1986.CrossRefMathSciNetGoogle Scholar
  12. 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. 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. 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. 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. 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. 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. 18.
    J.-J. Lévy. Optimal Reductions in the Lambda-Calculus, pages 159–191. Academic Press, 1980.Google Scholar
  19. 19.
    I. Mackie. The Geometry of Implementation. PhD thesis, University of London, September 1994.Google Scholar
  20. 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. 21.
    C.R. Murthy. Extracting Constructive Content from Classical Proofs. PhD thesis, Cornell University, August 1990.Google Scholar
  22. 22.
    S. Nishizaki. Programs with continuations and linear logic. Science of Computer Programming, 21(2):165–190, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  23. 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. 24.
    G. D. Plotkin. Call-by-name, call-by-value and the lambda calculus. Theoretical Computer Science, 1:125–159, 1975.zbMATHCrossRefMathSciNetGoogle Scholar
  25. 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. 26.
    H. Schellinx. The Noble Art of Linear Decorating. PhD thesis, Institute for Logic, Language and Computation, University of Amsterdam, 1994.Google Scholar
  27. 27.
    D. Sitaram and M. Felleisen. Control delimiters and their hierarchies. Lisp and Symbolic Computation, 3(1):67–99, January 1990CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Julia L. Lawall
    • 1
  • Harry G. Mairson
    • 1
  1. 1.Department of Computer ScienceBoston UniversityBoston

Personalised recommendations