Classical Call-by-Need and Duality

  • Zena M. Ariola
  • Hugo Herbelin
  • Alexis Saurin
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6690)


We study call-by-need from the point of view of the duality between call-by-name and call-by-value. We develop sequent-calculus style versions of call-by-need both in the minimal and classical case. As a result, we obtain a natural extension of call-by-need with control operators. This leads us to introduce a call-by-need λμ-calculus. Finally, by using the dualities principles of \(\overline\lambda\mu\tilde\mu \)-calculus, we show the existence of a new call-by-need calculus, which is distinct from call-by-name, call-by-value and usual call-by-need theories.


call-by-need lazy evaluation duality of computation sequent calculus λμ-calculus classical logic control subtraction connective 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Ariola, Z., Herbelin, H.: Minimal classical logic and control operators. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, Springer, Heidelberg (2003)Google Scholar
  2. 2.
    Ariola, Z.M., Bohannon, A., Sabry, A.: Sequent calculi and abstract machines. Transactions on Programming Languages and Systems (TOPLAS) 31(4), 275–317 (2009)Google Scholar
  3. 3.
    Ariola, Z.M., Felleisen, M.: The call-by-need lambda calculus. J. Funct. Program. 7(3), 265–301 (1997)CrossRefzbMATHGoogle Scholar
  4. 4.
    Ariola, Z.M., Herbelin, H.: Control reduction theories: the benefit of structural substitution. J. Funct. Program. 18(3), 373–419 (2008)CrossRefzbMATHGoogle Scholar
  5. 5.
    Ariola, Z.M., Herbelin, H., Sabry, A.: A proof-theoretic foundation of abortive continuations. Higher Order Symbol. Comput. 20, 403–429 (2007)CrossRefzbMATHGoogle Scholar
  6. 6.
    Ariola, Z.M., Herbelin, H., Sabry, A.: A type-theoretic foundation of delimited continuations. Higher Order Symbol. Comput. 22, 233–273 (2009)CrossRefzbMATHGoogle Scholar
  7. 7.
    Barendregt, H., Ghilezan, S.: Lambda terms for natural deduction, sequent calculus and cut elimination. J. Funct. Program. 10, 121–134 (2000)CrossRefzbMATHGoogle Scholar
  8. 8.
    Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984)zbMATHGoogle Scholar
  9. 9.
    Church, A.: A set of postulates for the foundation of logic. Annals of Mathematics 2(33), 346–366 (1932)CrossRefzbMATHGoogle Scholar
  10. 10.
    Crolard, T.: Subtractive Logic. Theoretical Computer Science 254(1-2), 151–185 (2001)CrossRefzbMATHGoogle Scholar
  11. 11.
    Curien, P.-L., Herbelin, H.: The duality of computation. In: International Conference on Functional Programming, pp. 233–243 (2000)Google Scholar
  12. 12.
    Danos, V., Joinet, J.-B., Schellinx, H.: LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of the classical implication. In: Advances in Linear Logic, vol. 222, pp. 211–224. Cambridge University Press, Cambridge (1995)CrossRefGoogle Scholar
  13. 13.
    Danos, V., Joinet, J.-B., Schellinx, H.: A new deconstructive logic: Linear logic. J. Symb. Log. 62(3), 755–807 (1997)CrossRefzbMATHGoogle Scholar
  14. 14.
    Danvy, O., Millikin, K., Munk, J., Zerny, I.: Defunctionalized interpreters for call-by-need evaluation. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 240–256. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  15. 15.
    David, R., Py, W.: Lambda-mu-calculus and Böhm’s theorem. J. Symb. Log. 66(1), 407–413 (2001)CrossRefzbMATHGoogle Scholar
  16. 16.
    Fasel, J.H., Hudak, P., Peyton Jones, S., Wadler, P. (eds.): Haskell special issue. SIGPLAN Notices 27(5) (May 1992)Google Scholar
  17. 17.
    Felleisen, M., Friedman, D.: Control operators, the secd machine, and the lambda-calculus. In: Formal Description of Programming Concepts-III, pp. 193–217. North-Holland, Amsterdam (1986)Google Scholar
  18. 18.
    Felleisen, M., Friedman, D., Kohlbecker, E.: A syntactic theory of sequential control. Theoretical Computer Science 52(3), 205–237 (1987)CrossRefzbMATHGoogle Scholar
  19. 19.
    Felleisen, M., Friedman, D., Kohlbecker, E., Duba, B.: Reasoning with continuations. In: First Symposium on Logic and Computer Science, pp. 131–141 (1986)Google Scholar
  20. 20.
    Filinski, A.: Declarative Continuations and Categorical Duality. Master thesis, DIKU, Danmark (August 1989)Google Scholar
  21. 21.
    Garcia, R., Lumsdaine, A., Sabry, A.: Lazy evaluation and delimited control. In: POPL 2009: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 153–164. ACM, New York (2009)Google Scholar
  22. 22.
    Gentzen, G.: Investigations into logical deduction. In: Szabo, M. (ed.) Collected papers of Gerhard Gentzen, pp. 68–131. North-Holland, Amsterdam (1969)Google Scholar
  23. 23.
    Herbelin, H.: C’est maintenant qu’on calcule. In: Habilitation à diriger les reserches (2005)Google Scholar
  24. 24.
    Herbelin, H., Zimmermann, S.: An operational account of call-by-value minimal and classical λ-calculus in “natural deduction” form. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 142–156. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  25. 25.
    Lafont, Y., Reus, B., Streicher, T.: Continuations semantics or expressing implication by negation. Technical Report 9321, Ludwig-Maximilians-UniversitÃd’t, MÃijnchen (1993)Google Scholar
  26. 26.
    Maraist, J., Odersky, M., Wadler, P.: The call-by-need λ-calculus. J. Funct. Program. 8(3), 275–317 (1998)CrossRefzbMATHGoogle Scholar
  27. 27.
    Moggi, E.: Computational λ-calculus and monads. In: Logic in Computer Science (1989)Google Scholar
  28. 28.
    Niehren, J., Schwinghammer, J., Smolka, G.: A concurrent lambda calculus with futures. Theor. Comput. Sci. 364, 338–356 (2006)CrossRefzbMATHGoogle Scholar
  29. 29.
    Okasaki, C., Lee, P., Tarditi, D.: Call-by-need and continuation-passing style. In: Lisp and Symbolic Computation, pp. 57–81. Kluwer Academic Publishers, Dordrecht (1993)Google Scholar
  30. 30.
    Parigot, M.: Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  31. 31.
    Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theoretical Comput. Sci. 1, 125–159 (1975)CrossRefzbMATHGoogle Scholar
  32. 32.
    Prawitz, D.: Natural Deduction, a Proof-Theoretical Study. Almquist and Wiksell, Stockholm (1965)zbMATHGoogle Scholar
  33. 33.
    Ronchi Della Rocca, S., Paolini, L.: The Parametric λ-Calculus: a Metamodel for Computation. Texts in Theoretical Computer Science: An EATCS Series. Springer, Heidelberg (2004)CrossRefzbMATHGoogle Scholar
  34. 34.
    Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation 6(3-4), 289–360 (1993)CrossRefGoogle Scholar
  35. 35.
    Saurin, A.: Separation with streams in the λμ-calculus. In: Proceedings of 20th IEEE Symposium on Logic in Computer Science (LICS 2005), Chicago, IL, USA, June 26-29, pp. 356–365. IEEE Computer Society, Los Alamitos (2005)Google Scholar
  36. 36.
    Selinger, P.: Control categories and duality: on the categorical semantics of the lambda-mu calculus. Mathematical Structures in Computer Science 11(2), 207–260 (2001)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Zena M. Ariola
    • 1
  • Hugo Herbelin
    • 2
  • Alexis Saurin
    • 2
  1. 1.University of OregonUSA
  2. 2.Laboratoire PPS, équipe π r2, CNRS, INRIA & Université Paris DiderotFrance

Personalised recommendations