This paper explores how the intersection type theories of call-by-name (CBN) and call-by-value (CBV) can be unified in a more general framework provided by call-by-push-value (CBPV). Indeed, we propose tight type systems for CBN and CBV that can be both encoded in a unique tight type system for CBPV. All such systems are quantitative, i.e. they provide exact information about the length of normalization sequences to normal form as well as the size of these normal forms. Moreover, the length of reduction sequences are discriminated according to their multiplicative and exponential nature, a concept inherited from linear logic. Last but not least, it is possible to extract quantitative measures for CBN and CBV from their corresponding encodings in CBPV. Call-by-Push-Value Call-by-Name Call-by-Value Intersection Types Theory of computation 27:1-27:20 Regular Paper This work has been partially supported by IRP SINFIN. https://arxiv.org/abs/2105.00564 We are specially grateful to G. Guerrieri for fruitful discussions. We also thank B. Accattoli, A. Bucciarelli, and A. Ríos for constructive remarks. Delia Kesner Delia Kesner Université de Paris, CNRS, IRIF, France Institut Universitaire de France (IUF), France https://orcid.org/0000-0003-4254-3129 Andrés Viso Andrés Viso Inria, Paris, France https://orcid.org/0000-0002-6822-8453 10.4230/LIPIcs.CSL.2022.27 Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds. PACMPL, 2(ICFP):94:1-94:30, 2018. URL: https://doi.org/10.1145/3236789. https://doi.org/10.1145/3236789 Beniamino Accattoli and Giulio Guerrieri. Open call-by-value. In Atsushi Igarashi, editor, Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, volume 10017 of Lecture Notes in Computer Science, pages 206-226, 2016. URL: https://doi.org/10.1007/978-3-319-47958-3_12. https://doi.org/10.1007/978-3-319-47958-3_12 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. https://doi.org/10.1007/978-3-030-02768-1_3 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. https://doi.org/10.1007/978-3-030-17184-1_15 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. https://doi.org/10.1007/978-3-642-15205-4_30 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. https://doi.org/10.1007/978-3-642-29822-6_4 Sandra Alves, Delia Kesner, and Daniel Ventura. A quantitative understanding of pattern matching. In Marc Bezem and Assia Mahboubi, editors, 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway, volume 175 of LIPIcs, pages 3:1-3:36. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.TYPES.2019.3. https://doi.org/10.4230/LIPIcs.TYPES.2019.3 Hendrik P. Barendregt. The Lambda Calculus Its Syntax and Semantics, volume 103. North Holland, revised edition, 1984. 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. https://doi.org/10.2168/LMCS-9(4:3)2013 Marc Bezem, Jan Willem Klop, and Vincent van Oostrom. Term Rewriting Systems (TeReSe). Cambridge University Press, 2003. Antonio Bucciarelli and Thomas Ehrhard. On phase semantics and denotational semantics: the exponentials. Ann. Pure Appl. Logic, 109(3):205-241, 2001. URL: https://doi.org/10.1016/S0168-0072(00)00056-7. https://doi.org/10.1016/S0168-0072(00)00056-7 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. https://doi.org/10.1007/978-3-030-59025-3_2 Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Solvability = typability + inhabitation. Log. Methods Comput. Sci., 17(1), 2021. URL: https://lmcs.episciences.org/7141. https://lmcs.episciences.org/7141 Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Logic Journal of the IGPL, 25(4):431-464, 2017. URL: https://doi.org/10.1093/jigpal/jzx018. https://doi.org/10.1093/jigpal/jzx018 Alberto Carraro and Giulio Guerrieri. A semantical and operational account of call-by-value solvability. In Anca Muscholl, editor, Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8412 of Lecture Notes in Computer Science, pages 103-118. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54830-7_7. https://doi.org/10.1007/978-3-642-54830-7_7 Jules Chouquet and Christine Tasson. Taylor expansion for call-by-push-value. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain, volume 152 of LIPIcs, pages 16:1-16:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.16. https://doi.org/10.4230/LIPIcs.CSL.2020.16 Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In Martin Odersky and Philip Wadler, editors, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), Montreal, Canada, September 18-21, 2000, pages 233-243. ACM, 2000. URL: https://doi.org/10.1145/351240.351262. https://doi.org/10.1145/351240.351262 Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. Sequent calculi for second order logic. In Jean-Yves Girard, Yves Lafont, and Laurent Regnier, editors, Advances in Linear Logic. Cambridge University Press, 1995. Daniel de Carvalho. Sémantiques de la logique linéaire et temps de calcul. PhD thesis, Université Aix-Marseille II, 2007. Daniel de Carvalho. The relational model is injective for multiplicative exponential linear logic. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 41:1-41:19. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.41. https://doi.org/10.4230/LIPIcs.CSL.2016.41 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. https://doi.org/10.1017/S0960129516000396 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. https://doi.org/10.1016/j.ic.2015.12.010 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. https://doi.org/10.1016/j.tcs.2010.12.017 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 fuer Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.CSL.2012.259. https://doi.org/10.4230/LIPIcs.CSL.2012.259 Thomas Ehrhard. Call-by-push-value from a linear logic point of view. In Peter Thiemann, editor, Programming Languages and Systems - 25th European Symposium on Programming, ESOP 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 9632 of Lecture Notes in Computer Science, pages 202-228. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_9. https://doi.org/10.1007/978-3-662-49498-1_9 Thomas Ehrhard and Giulio Guerrieri. The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In James Cheney and Germán Vidal, editors, Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016, pages 174-187. ACM, 2016. URL: https://doi.org/10.1145/2967973.2968608. https://doi.org/10.1145/2967973.2968608 Claudia Faggian and Giulio Guerrieri. Factorization in call-by-name and call-by-value calculi via linear logic. In Stefan Kiefer and Christine Tasson, editors, Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, volume 12650 of Lecture Notes in Computer Science, pages 205-225. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-71995-1_11. https://doi.org/10.1007/978-3-030-71995-1_11 Philippa Gardner. Discovering needed reductions using type theory. In Masami Hagiya and John C. Mitchell, editors, Theoretical Aspects of Computer Software, International Conference TACS '94, Sendai, Japan, April 19-22, 1994, Proceedings, volume 789 of Lecture Notes in Computer Science, pages 555-574. Springer, 1994. URL: https://doi.org/10.1007/3-540-57887-0_115. https://doi.org/10.1007/3-540-57887-0_115 Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4. https://doi.org/10.1016/0304-3975(87)90045-4 Jean-Yves Girard. Normal functors, power series and λ-calculus. Ann. Pure Appl. Logic, 37(2):129-177, 1988. URL: https://doi.org/10.1016/0168-0072(88)90025-5. https://doi.org/10.1016/0168-0072(88)90025-5 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. https://doi.org/10.4204/EPTCS.293.5 Giulio Guerrieri and Giulio Manzonetto. The bang calculus and the two girard’s translations. In Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity-TLLA), Oxford, UK, 7-8 July 2018., EPTCS, pages 15-30, 2019. Giulio Guerrieri, Luc Pellissier, and Lorenzo Tortora de Falco. Computing connected proof(-structure)s from their taylor expansion. In Delia Kesner and Brigitte Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal, volume 52 of LIPIcs, pages 20:1-20:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.FSCD.2016.20. https://doi.org/10.4230/LIPIcs.FSCD.2016.20 Axel Kerinec, Giulio Manzonetto, and Simona Ronchi Della Rocca. Call-by-value, again! In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 7:1-7:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.7. https://doi.org/10.4230/LIPIcs.FSCD.2021.7 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 fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.24. https://doi.org/10.4230/LIPIcs.FSCD.2017.24 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. https://doi.org/10.1145/3373718.3394774 Delia Kesner and Andrés Viso. Encoding tight typing in a unified framework. CoRR, abs/2105.00564, 2021. URL: http://arxiv.org/abs/2105.00564. http://arxiv.org/abs/2105.00564 Zurab Khasidashvili. The Church-Rosser theorem in orthogonal combinatory reduction systems. Technical Report 1825, INRIA Rocquencourt, France, 1992. Jan Willem Klop. Combinatory reduction systems. PhD thesis, Univ. Utrecht, 1980. Maico Leberle. Dissecting call-by-need by customizing multi type systems. PhD thesis, Institut Polytechnique de Paris, 2021. Paul Blain Levy. Call-By-Push-Value: A Functional/Imperative Synthesis, volume 2 of Semantics Structures in Computation. Springer, 2004. Paul Blain Levy. Call-by-push-value: Decomposing call-by-value and call-by-name. Higher-Order and Symbolic Computation, 19(4):377-414, 2006. URL: https://doi.org/10.1007/s10990-006-0480-6. https://doi.org/10.1007/s10990-006-0480-6 Giulio Manzonetto, Michele Pagani, and Simona Ronchi Della Rocca. New semantical insights into call-by-value λ-calculus. Fundam. Informaticae, 170(1-3):241-265, 2019. URL: https://doi.org/10.3233/FI-2019-1862. https://doi.org/10.3233/FI-2019-1862 Damiano Mazza, Luc Pellissier, and Pierre Vial. Polyadic approximations, fibrations and intersection types. Proc. ACM Program. Lang., 2(POPL):6:1-6:28, 2018. URL: https://doi.org/10.1145/3158094. https://doi.org/10.1145/3158094 Laurent Regnier. Une équivalence sur les lambda-termes. TCS, 2(126):281-292, 1994. José Espírito Santo, Luís Pinto, and Tarmo Uustalu. Modal embeddings and calling paradigms. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany., volume 131 of LIPIcs, pages 18:1-18:20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.18. https://doi.org/10.4230/LIPIcs.FSCD.2019.18 Delia Kesner and Andrés Viso Creative Commons Attribution 4.0 International license https://creativecommons.org/licenses/by/4.0/legalcode 2022-01-27