Document Open Access Logo

Useful Call-by-Value: A Semantic Interpretation via Quantitative Types

Authors Pablo Barenbaum , Delia Kesner , Mariana Milicich

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.47.pdf
  • Filesize: 0.97 MB
  • 24 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Type theory
  • Theory of computation → Operational semantics
Keywords
  • Lambda calculus
  • Evaluation strategies
  • Call-by-Value
  • Useful Evaluation
  • Intersection types
  • Quantitative models

Metrics

Abstract

Useful evaluation is an optimised evaluation mechanism for functional programming languages. It relies on representing terms with sharing and imposing a restricted notion of useful substitutions, that intuitively disallows copying subterms that do not contribute to the progress of the computation.
In particular, useful call-by-value evaluation optimises the standard call-by-value strategy by preserving its original semantics. This preservation result has been shown by means of syntactical rewriting techniques, difficult to adapt to alternative variants of the calculi at play.
In this work, we present the first semantic model of useful call-by-value evaluation through the non-idempotent intersection type system 𝒰. Our first contribution is a characterisation of termination for useful call-by-value evaluation via system 𝒰. That is, a term is typable in system 𝒰 if and only if it terminates in the useful call-by-value strategy. As a second contribution, we show that system 𝒰 provides a quantitative interpretation for useful call-by-value evaluation, offering exact step-count information for program evaluation. Our third contribution is that termination in call-by-value and useful call-by-value are equivalent. This ensures in particular that call-by-value, which is (potentially) erasing, and useful call-by-value, which is non-erasing, are observationally equivalent. Even though the specification of the operational semantics of useful evaluation is highly complex, system 𝒰 is notably simple. As far as we know, system 𝒰 is one of the scarce quantitative type systems capturing exactly the substitution step-count for variables and abstractions in an open call-by-value strategy.

Cite As Get BibTex

Pablo Barenbaum, Delia Kesner, and Mariana Milicich. Useful Call-by-Value: A Semantic Interpretation via Quantitative Types. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 47:1-47:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.47

Author Details

Pablo Barenbaum
  • Universidad Nacional de Quilmes (CONICET), Buenos Aires, Argentina
  • Instituto de Ciencias de la Computación, UBA, Buenos Aires, Argentina
Delia Kesner
  • Université Paris Cité, CNRS, IRIF, France
Mariana Milicich
  • Université Paris Cité, CNRS, IRIF, France

Funding

This work was supported by the European Union through the MSCA SE project QCOMICAL (Grant Agreement ID: 101182520).
  • Milicich, Mariana: This project has received funding from the EU Horizon 2020 research and innovation programme MSCA No 945332.

References

  1. Beniamino Accattoli and Claudio Sacerdoti Coen. On the relative usefulness of fireballs. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 141-155. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.23.
  2. Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds. Proc. ACM Program. Lang., 2(ICFP):94:1-94:30, 2018. URL: https://doi.org/10.1145/3236789.
  3. Beniamino Accattoli and Giulio Guerrieri. Implementing open call-by-value. In Mehdi Dastani and Marjan Sirjani, editors, Fundamentals of Software Engineering - 7th International Conference, FSEN 2017, Tehran, Iran, April 26-28, 2017, Revised Selected Papers, volume 10522 of Lecture Notes in Computer Science, pages 1-19. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-68972-2_1.
  4. Beniamino Accattoli and Giulio Guerrieri. Types of fireballs. In Sukyoung Ryu, editor, Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings, volume 11275 of Lecture Notes in Computer Science, pages 45-66. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02768-1_3.
  5. Beniamino Accattoli and Giulio Guerrieri. Abstract machines for open call-by-value. Sci. Comput. Program., 184, 2019. URL: https://doi.org/10.1016/J.SCICO.2019.03.002.
  6. Beniamino Accattoli and Giulio Guerrieri. The theory of call-by-value solvability. Proc. ACM Program. Lang., 6(ICFP):855-885, 2022. URL: https://doi.org/10.1145/3547652.
  7. Beniamino Accattoli, Giulio Guerrieri, and Maico Leberle. Types by need. In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 410-439. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_15.
  8. Beniamino Accattoli and Delia Kesner. The structural lambda-calculus. In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 381-395. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15205-4_30.
  9. Beniamino Accattoli and Ugo Dal Lago. Beta reduction is invariant, indeed. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 8:1-8:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603105.
  10. Beniamino Accattoli and Luca Paolini. Call-by-value solvability, revisited. In Tom Schrijvers and Peter Thiemann, editors, Functional and Logic Programming - 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings, volume 7294 of Lecture Notes in Computer Science, pages 4-16. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-29822-6_4.
  11. Sandra Alves, Delia Kesner, and Miguel Ramos. Quantitative global memory. In Helle Hvid Hansen and Andre Scedrov, editors, Logic, Language, Information, and Computation - 29th International Workshop, WoLLIC 2023, Halifax, Canada, September 20-23, 2023, Proceedings, Lecture Notes in Computer Science, 2023. Google Scholar
  12. Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. The call-by-need lambda calculus. In Ron K. Cytron and Peter Lee, editors, Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, pages 233-246. ACM Press, 1995. URL: https://doi.org/10.1145/199448.199507.
  13. Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, and Delia Kesner. Foundations of strong call by need. Proc. ACM Program. Lang., 1(ICFP):20:1-20:29, 2017. URL: https://doi.org/10.1145/3110264.
  14. Pablo Barenbaum, Eduardo Bonelli, and Kareem Mohamed. Pattern matching and fixed points: Resource types and strong call-by-need: Extended abstract. In David Sabel and Peter Thiemann, editors, Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, pages 6:1-6:12. ACM, 2018. URL: https://doi.org/10.1145/3236950.3236972.
  15. Pablo Barenbaum, Delia Kesner, and Mariana Milicich. A fresh inductive approach to useful call-by-value. In Clark W. Barrett and Uwe Waldmann, editors, Automated Deduction - CADE 30 - 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings, volume 15943 of Lecture Notes in Computer Science, pages 381-399. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-99984-0_21.
  16. Pablo Barenbaum, Delia Kesner, and Mariana Milicich. Useful evaluation: Syntax and semantics (technical report), 2025. URL: https://arxiv.org/abs/2404.18874.
  17. Alexis Bernadet and Stéphane Lengrand. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science, 9(4), 2013. URL: https://doi.org/10.2168/LMCS-9(4:3)2013.
  18. Antonio Bucciarelli and Thomas Ehrhard. On phase semantics and denotational semantics: the exponentials. Ann. Pure Appl. Log., 109(3):205-241, 2001. URL: https://doi.org/10.1016/S0168-0072(00)00056-7.
  19. Antonio Bucciarelli, Delia Kesner, Alejandro Ríos, and Andrés Viso. The bang calculus revisited. In Keisuke Nakano and Konstantinos Sagonas, editors, Functional and Logic Programming - 15th International Symposium, FLOPS 2020, Akita, Japan, September 14-16, 2020, Proceedings, volume 12073 of Lecture Notes in Computer Science, pages 13-32. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-59025-3_2.
  20. Antonio Bucciarelli, Delia Kesner, Alejandro Ríos, and Andrés Viso. The bang calculus revisited. Inf. Comput., 293:105047, 2023. URL: https://doi.org/10.1016/J.IC.2023.105047.
  21. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Log. J. IGPL, 25(4):431-464, 2017. URL: https://doi.org/10.1093/JIGPAL/JZX018.
  22. Daniel de Carvalho. Sémantiques de la logique linéaire et temps de calcul. PhD thesis, Ecole Doctorale Physique et Sciences de la Matière (Marseille), 2007. Google Scholar
  23. Mario Coppo and Mariangiola Dezani-Ciancaglini. A new type assignment for λ-terms. Arch. Math. Log., 19(1):139-156, 1978. URL: https://doi.org/10.1007/BF02011875.
  24. Mario Coppo and Mariangiola Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame J. Formal Log., 21(4):685-693, 1980. URL: https://doi.org/10.1305/NDJFL/1093883253.
  25. Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Mathematical Structures in Computer Science, 28(7):1169-1203, 2018. URL: https://doi.org/10.1017/S0960129516000396.
  26. Daniel de Carvalho and Lorenzo Tortora de Falco. A semantic account of strong normalization in linear logic. Inf. Comput., 248:104-129, 2016. URL: https://doi.org/10.1016/J.IC.2015.12.010.
  27. Daniel de Carvalho, Michele Pagani, and Lorenzo Tortora de Falco. A semantic measure of the execution time in linear logic. Theor. Comput. Sci., 412(20):1884-1902, 2011. URL: https://doi.org/10.1016/J.TCS.2010.12.017.
  28. Thomas Ehrhard. Collapsing non-idempotent intersection types. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France, volume 16 of LIPIcs, pages 259-273. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.CSL.2012.259.
  29. Álvaro García-Pérez and Pablo Nogueira. No solvable lambda-value term left behind. Log. Methods Comput. Sci., 12(2), 2016. URL: https://doi.org/10.2168/LMCS-12(2:12)2016.
  30. Philippa Gardner. Discovering needed reductions using type theory. In Theoretical Aspects of Computer Software, pages 555-574. Springer, 1994. URL: https://doi.org/10.1007/3-540-57887-0_115.
  31. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  32. Jean-Yves Girard. Normal functors, power series and λ-calculus. Ann. Pure Appl. Log., 37(2):129-177, 1988. URL: https://doi.org/10.1016/0168-0072(88)90025-5.
  33. Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In Mitchell Wand and Simon L. Peyton Jones, editors, Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002, pages 235-246. ACM, 2002. URL: https://doi.org/10.1145/581478.581501.
  34. Giulio Guerrieri. Towards a semantic measure of the execution time in call-by-value lambda-calculus. In Michele Pagani and Sandra Alves, editors, Proceedings Twelfth Workshop on Developments in Computational Models and Ninth Workshop on Intersection Types and Related Systems, DCM/ITRS 2018, Oxford, UK, 8th July 2018, volume 293 of EPTCS, pages 57-72, 2018. URL: https://doi.org/10.4204/EPTCS.293.5.
  35. Delia Kesner. A theory of explicit substitutions with safe and full composition. Logical Methods in Computer Science, 5(3), 2009. URL: http://arxiv.org/abs/0905.2539.
  36. Delia Kesner. Reasoning about call-by-need by means of types. In Bart Jacobs and Christof Löding, editors, Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9634 of Lecture Notes in Computer Science, pages 424-441. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49630-5_25.
  37. Delia Kesner and Pierre Vial. Types as resources for classical natural deduction. In Dale Miller, editor, 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK, volume 84 of LIPIcs, pages 24:1-24:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.24.
  38. Delia Kesner and Pierre Vial. Consuming and persistent types for classical logic. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 619-632. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394774.
  39. Delia Kesner and Andrés Viso. Encoding tight typing in a unified framework. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPIcs, pages 27:1-27:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.27.
  40. Maico Leberle. Dissecting call-by-need by customizing multi type systems. (Une dissection de l'appel-par-nécessité par la personnalisation des systèmes de multi types). PhD thesis, IP Paris, France, 2021. URL: https://tel.archives-ouvertes.fr/tel-03284370.
  41. John Maraist, Martin Odersky, David N. Turner, and Philip Wadler. Call-by-name, call-by-value, call-by-need and the linear lambda calculus. In Stephen D. Brookes, Michael G. Main, Austin Melton, and Michael W. Mislove, editors, Eleventh Annual Conference on Mathematical Foundations of Programming Semantics, MFPS 1995, Tulane University, New Orleans, LA, USA, March 29 - April 1, 1995, volume 1 of Electronic Notes in Theoretical Computer Science, pages 370-392. Elsevier, 1995. URL: https://doi.org/10.1016/S1571-0661(04)00022-2.
  42. Luca Paolini and Simona Ronchi Della Rocca. Call-by-value solvability. RAIRO Theor. Informatics Appl., 33(6):507-534, 1999. URL: https://doi.org/10.1051/ITA:1999130.
  43. Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci., 1(2):125-159, 1975. URL: https://doi.org/10.1016/0304-3975(75)90017-1.
  44. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  45. Jui-Hsuan Wu. Proofs as terms, terms as graphs. In Chung-Kil Hur, editor, Programming Languages and Systems - 21st Asian Symposium, APLAS 2023, Taipei, Taiwan, November 26-29, 2023, Proceedings, volume 14405 of Lecture Notes in Computer Science, pages 91-111. Springer, 2023. URL: https://doi.org/10.1007/978-981-99-8311-7_5.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact