Open Call-by-Value | SpringerLink
Skip to main content
Springer Nature Link
Log in

Open Call-by-Value

  • Conference paper
  • First Online:
Programming Languages and Systems (APLAS 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10017))

Included in the following conference series:

Abstract

The elegant theory of the call-by-value lambda-calculus relies on weak evaluation and closed terms, that are natural hypotheses in the study of programming languages. To model proof assistants, however, strong evaluation and open terms are required, and it is well known that the operational semantics of call-by-value becomes problematic in this case. Here we study the intermediate setting—that we call Open Call-by-Value—of weak evaluation with open terms, on top of which Grégoire and Leroy designed the abstract machine of Coq. Various calculi for Open Call-by-Value already exist, each one with its pros and cons. This paper presents a detailed comparative study of the operational semantics of four of them, coming from different areas such as the study of abstract machines, denotational semantics, linear logic proof nets, and sequent calculus. We show that these calculi are all equivalent from a termination point of view, justifying the slogan Open Call-by-Value.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Accattoli, B., Sacerdoti Coen, C.: On the relative usefulness of fireballs. In: LICS 2015, pp. 141–155 (2015)

    Google Scholar 

  2. Accattoli, B.: Proof nets and the call-by-value \(\lambda \)-calculus. Theor. Comput. Sci. 606, 2–24 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  3. Accattoli, B., Guerrieri, G.: Open call-by-value (Extended Version). CoRR abs/1609.00322 (2016). http://arxiv.org/abs/1609.00322

    Google Scholar 

  4. Accattoli, B., Paolini, L.: Call-by-value solvability, revisited. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol. 7294, pp. 4–16. Springer, Heidelberg (2012). doi:10.1007/978-3-642-29822-6_4

    Chapter  Google Scholar 

  5. Accattoli, B., Sacerdoti Coen, C.: On the value of variables. In: WoLLIC 2014, pp. 36–50 (2014)

    Google Scholar 

  6. Ariola, Z.M., Bohannon, A., Sabry, A.: Sequent calculi and abstract machines. ACM Trans. Program. Lang. Syst. 31(4), 13:1–13:48 (2009)

    Article  Google Scholar 

  7. Blelloch, G.E., Greiner, J.: Parallelism in sequential functional languages. In: FPCA, pp. 226–237 (1995)

    Google Scholar 

  8. Carraro, A., Guerrieri, G.: A semantical and operational account of call-by-value solvability. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 103–118. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54830-7_7

    Chapter  Google Scholar 

  9. Curien, P.L., Herbelin, H.: The duality of computation. In: ICFP, pp. 233–243 (2000)

    Google Scholar 

  10. Curien, P.-L., Munch-Maccagnoni, G.: The duality of computation under focus. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IAICT, vol. 323, pp. 165–181. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15240-5_13

    Chapter  Google Scholar 

  11. Dal Lago, U., Martini, S.: The weak lambda calculus as a reasonable machine. Theor. Comput. Sci. 398(1–3), 32–50 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  12. Dyckhoff, R., Lengrand, S.: Call-by-value lambda-calculus and LJQ. J. Log. Comput. 17(6), 1109–1134 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  13. Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: ICFP 2002, pp. 235–246 (2002)

    Google Scholar 

  14. Guerrieri, G.: Head reduction and normalization in a call-by-value lambda-calculus. In: WPTE 2015, pp. 3–17 (2015)

    Google Scholar 

  15. Guerrieri, G., Paolini, L., Ronchi Della Rocca, S.: Standardization of a call-by-value lambda-calculus. In: TLCA 2015, pp. 211–225 (2015)

    Google Scholar 

  16. Herbelin, H., Zimmermann, S.: An operational account of call-by-value minimal and classical \(\lambda \)-calculus in natural deduction form. In: TLCA, pp. 142–156 (2009)

    Google Scholar 

  17. Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall Inc., Upper Saddle River (1993)

    MATH  Google Scholar 

  18. Lassen, S.: Eager normal form bisimulation. In: LICS 2005, pp. 345–354 (2005)

    Google Scholar 

  19. Lévy, J.J.: Réductions correctes et optimales dans le lambda-calcul. Thése d’Etat, Univ. Paris VII, France (1978)

    Google Scholar 

  20. Maraist, J., Odersky, M., Turner, D.N., Wadler, P.: Call-by-name, call-by-value, call-by-need and the linear \(\lambda \)-calculus. TCS 228(1–2), 175–210 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  21. Moggi, E.: Computational \(\lambda \)-calculus and Monads. In: LICS 1989, pp. 14–23 (1989)

    Google Scholar 

  22. Paolini, L., Pimentel, E., Ronchi Della Rocca, S.: Strong normalization from an unusual point of view. Theor. Comput. Sci. 412(20), 1903–1915 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  23. Paolini, L.: Call-by-value separability and computability. In: ICTCS, pp. 74–89 (2002)

    Google Scholar 

  24. Paolini, L., Pimentel, E., Ronchi Della Rocca, S.: Lazy strong normalization. In: ITRS 2004. Electronic Notes in Theoretical Computer Science, vol. 136C, pp. 103–116 (2005)

    Google Scholar 

  25. Paolini, L., Ronchi Della Rocca, S.: Call-by-value solvability. ITA 33(6), 507–534 (1999)

    MathSciNet  MATH  Google Scholar 

  26. Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125–159 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  27. Regnier, L.: Une équivalence sur les lambda-termes. TCS 2(126), 281–292 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  28. Ronchi Della Rocca, S., Paolini, L.: The Parametric \(\lambda \)-Calculus. Springer, Heidelberg (2004)

    Google Scholar 

  29. Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. Lisp Symbolic Comput. 6(3–4), 289–360 (1993)

    Article  Google Scholar 

  30. Sabry, A., Wadler, P.: A reflection on call-by-value. ACM Trans. Program. Lang. Syst. 19(6), 916–941 (1997)

    Article  MATH  Google Scholar 

  31. Sands, D., Gustavsson, J., Moran, A.: Lambda calculi and linear speedups. In: The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, pp. 60–84 (2002)

    Google Scholar 

Download references

Acknowledgment

Work partially supported by the A*MIDEX project ANR-11-IDEX-0001-02 funded by the “Investissements d’Avenir” French Government program, managed by the French National Research Agency (ANR), and by ANR projects ANR-12-JS02-006-01 (CoQuaS) and ANR-11-IS02-0002 (Locali).

Author information

Authors and Affiliations

  1. Inria, UMR 7161, LIX, École Polytechnique, Palaiseau, France

    Beniamino Accattoli

  2. Aix Marseille Univ, CNRS, Centrale Marseille, I2M, Marseille, France

    Giulio Guerrieri

Authors
  1. Beniamino Accattoli
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Giulio Guerrieri
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Beniamino Accattoli .

Editor information

Editors and Affiliations

  1. Kyoto University , Kyoto, Japan

    Atsushi Igarashi

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Accattoli, B., Guerrieri, G. (2016). Open Call-by-Value. In: Igarashi, A. (eds) Programming Languages and Systems. APLAS 2016. Lecture Notes in Computer Science(), vol 10017. Springer, Cham. https://doi.org/10.1007/978-3-319-47958-3_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47958-3_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-47957-6

  • Online ISBN: 978-3-319-47958-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation