Advertisement

Implementing Open Call-by-Value

  • Beniamino Accattoli
  • Giulio GuerrieriEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10522)

Abstract

The 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. Open call-by-value is the intermediate setting of weak evaluation with open terms, on top of which Grégoire and Leroy designed the abstract machine of Coq. This paper provides a theory of abstract machines for open call-by-value. The literature contains machines that are either simple but inefficient, as they have an exponential overhead, or efficient but heavy, as they rely on a labelling of environments and a technical optimization. We introduce a machine that is simple and efficient: it does not use labels and it implements open call-by-value within a bilinear overhead. Moreover, we provide a new fine understanding of how different optimizations impact on the complexity of the overhead.

Notes

Acknowledgements

This work has been partially funded by the ANR JCJC grant COCA HOLA (ANR-16-CE40-004-01).

References

  1. 1.
    Abramsky, S., Ong, C.L.: Full abstraction in the lazy lambda calculus. Inf. Comput. 105(2), 159–267 (1993)CrossRefzbMATHMathSciNetGoogle Scholar
  2. 2.
    Accattoli, B., Sacerdoti Coen, C.: On the relative usefulness of fireballs. In: LICS 2015, pp. 141–155 (2015)Google Scholar
  3. 3.
    Accattoli, B.: The useful MAM, a reasonable implementation of the strong \(\lambda \)-Calculus. In: Väänänen, J., Hirvonen, Å., de Queiroz, R. (eds.) WoLLIC 2016. LNCS, vol. 9803, pp. 1–21. Springer, Heidelberg (2016). doi: 10.1007/978-3-662-52921-8_1 Google Scholar
  4. 4.
    Accattoli, B.: The complexity of abstract machines. In: WPTE 2016 (invited paper), pp. 1–15 (2017)Google Scholar
  5. 5.
    Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: ICFP 2014, pp. 363–376 (2014)Google Scholar
  6. 6.
    Accattoli, B., Barenbaum, P., Mazza, D.: A strong distillery. In: Feng, X., Park, S. (eds.) APLAS 2015. LNCS, vol. 9458, pp. 231–250. Springer, Cham (2015). doi: 10.1007/978-3-319-26529-2_13 CrossRefGoogle Scholar
  7. 7.
    Accattoli, B., Dal Lago, U.: Beta reduction is invariant, indeed. In: CSL-LICS 2014. pp. 8:1–8:10 (2014)Google Scholar
  8. 8.
    Accattoli, B., Guerrieri, G.: Open call-by-value. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 206–226. Springer, Cham (2016). doi: 10.1007/978-3-319-47958-3_12 CrossRefGoogle Scholar
  9. 9.
    Accattoli, B., Guerrieri, G.: Implementing Open Call-by-Value (Extended Version). CoRR abs/1701.08186 (2017). https://arxiv.org/abs/1701.08186
  10. 10.
    Accattoli, B., Sacerdoti Coen, C.: On the value of variables. In: Kohlenbach, U., Barceló, P., Queiroz, R. (eds.) WoLLIC 2014. LNCS, vol. 8652, pp. 36–50. Springer, Heidelberg (2014). doi: 10.1007/978-3-662-44145-9_3 Google Scholar
  11. 11.
    Ariola, Z.M., Bohannon, A., Sabry, A.: Sequent calculi and abstract machines. ACM Trans. Program. Lang. Syst. 31(4), 13:1–13:48 (2009)Google Scholar
  12. 12.
    Blelloch, G.E., Greiner, J.: A provable time and space efficient implementation of NESL. In: ICFP 1996, pp. 213–225 (1996)Google Scholar
  13. 13.
    Crégut, P.: An abstract machine for lambda-terms normalization. In: LISP and Functional Programming, pp. 333–340 (1990)Google Scholar
  14. 14.
    Dal Lago, U., Martini, S.: Derivational complexity is an invariant cost model. In: Eekelen, M., Shkaravska, O. (eds.) FOPARA 2009. LNCS, vol. 6324, pp. 100–113. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-15331-0_7
  15. 15.
    Dal Lago, U., Martini, S.: On constructor rewrite systems and the lambda-calculus. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 163–174. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-02930-1_14
  16. 16.
    Danvy, O., Zerny, I.: A synthetic operational account of call-by-need evaluation. In: PPDP, pp. 97–108 (2013)Google Scholar
  17. 17.
    Fernández, M., Siafakas, N.: New developments in environment machines. Electr. Notes Theor. Comput. Sci. 237, 57–73 (2009)CrossRefzbMATHGoogle Scholar
  18. 18.
    Friedman, D.P., Ghuloum, A., Siek, J.G., Winebarger, O.L.: Improving the lazy Krivine machine. Higher-Order Symbolic Comput. 20(3), 271–293 (2007)CrossRefzbMATHGoogle Scholar
  19. 19.
    García-Pérez, Á., Nogueira, P., Moreno-Navarro, J.J.: Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order. In: PPDP, pp. 85–96 (2013)Google Scholar
  20. 20.
    Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: ICFP 2002, pp. 235–246 (2002)Google Scholar
  21. 21.
    Paolini, L., Ronchi Della Rocca, S.: Call-by-value Solvability. ITA 33(6), 507–534 (1999)zbMATHMathSciNetGoogle Scholar
  22. 22.
    Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125–159 (1975)CrossRefzbMATHGoogle Scholar
  23. 23.
    Ronchi Della Rocca, S., Paolini, L.: The Parametric \({\lambda }\)-Calculus - A Metamodel for Computation. Springer, Berlin (2004)Google Scholar
  24. 24.
    Sands, D., Gustavsson, J., Moran, A.: Lambda calculi and linear speedups. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 60–82. Springer, Heidelberg (2002). doi: 10.1007/3-540-36377-7_4 CrossRefGoogle Scholar
  25. 25.
    Sestoft, P.: Deriving a lazy abstract machine. J. Funct. Program. 7(3), 231–264 (1997)CrossRefzbMATHMathSciNetGoogle Scholar
  26. 26.
    Wand, M.: On the correctness of the Krivine machine. Higher-Order Symbolic Comput. 20(3), 231–235 (2007)CrossRefzbMATHGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2017

Authors and Affiliations

  1. 1.INRIA, UMR 7161, LIXÉcole PolytechniquePalaiseauFrance
  2. 2.Department of Computer ScienceUniversity of OxfordOxfordUK

Personalised recommendations