{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T11:40:47Z","timestamp":1761824447692,"version":"3.40.3"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031479625"},{"type":"electronic","value":"9783031479632"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-47963-2_13","type":"book-chapter","created":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T21:41:26Z","timestamp":1700689286000},"page":"196-215","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Strong Call-by-Value and\u00a0Multi Types"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4944-9944","authenticated-orcid":false,"given":"Beniamino","family":"Accattoli","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0469-4279","authenticated-orcid":false,"given":"Giulio","family":"Guerrieri","sequence":"additional","affiliation":[]},{"given":"Maico","family":"Leberle","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,11,23]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2015.08.006","volume":"606","author":"B Accattoli","year":"2015","unstructured":"Accattoli, B.: Proof nets and the call-by-value $$\\lambda $$-calculus. Theor. Comput. Sci. 606, 2\u201324 (2015). https:\/\/doi.org\/10.1016\/j.tcs.2015.08.006","journal-title":"Theor. Comput. Sci."},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Condoluci, A., Sacerdoti Coen, C.: Strong call-by-value is reasonable, implosively. In: LICS 2021. IEEE (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470630","DOI":"10.1109\/LICS52264.2021.9470630"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Faggian, C., Lancelot, A.: Normal form bisimulations by value. CoRR abs\/2303.08161 (2023). https:\/\/doi.org\/10.48550\/arXiv.2303.08161","DOI":"10.48550\/arXiv.2303.08161"},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Graham-Lengrand, S., Kesner, D.: Tight typings and split bounds. PACMPL 2(ICFP), 94:1\u201394:30 (2018). https:\/\/doi.org\/10.1145\/3236789","DOI":"10.1145\/3236789"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-319-47958-3_12","volume-title":"Programming Languages and Systems","author":"B Accattoli","year":"2016","unstructured":"Accattoli, B., Guerrieri, G.: Open call-by-value. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 206\u2013226. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47958-3_12"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-030-02768-1_3","volume-title":"Programming Languages and Systems","author":"B Accattoli","year":"2018","unstructured":"Accattoli, B., Guerrieri, G.: Types of fireballs. In: Ryu, S. (ed.) APLAS 2018. LNCS, vol. 11275, pp. 45\u201366. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02768-1_3"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Guerrieri, G.: Abstract machines for open call-by-value. Sci. Comput. Program. 184 (2019). https:\/\/doi.org\/10.1016\/j.scico.2019.03.002","DOI":"10.1016\/j.scico.2019.03.002"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Guerrieri, G.: The theory of call-by-value solvability. Proc. ACM Program. Lang. 6(ICFP), 855\u2013885 (2022). https:\/\/doi.org\/10.1145\/3547652","DOI":"10.1145\/3547652"},{"key":"13_CR9","unstructured":"Accattoli, B., Guerrieri, G., Leberle, M.: Semantic bounds and strong call-by-value normalization. CoRR abs\/2104.13979 (2021). https:\/\/arxiv.org\/abs\/2104.13979"},{"key":"13_CR10","unstructured":"Accattoli, B., Guerrieri, G., Leberle, M.: Strong call-by-value and multi types (long version). CoRR abs\/2309.12261 (2023). https:\/\/arxiv.org\/abs\/2309.12261"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-29822-6_4","volume-title":"Functional and Logic Programming","author":"B Accattoli","year":"2012","unstructured":"Accattoli, B., Paolini, L.: Call-by-value solvability, revisited. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol. 7294, pp. 4\u201316. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29822-6_4"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Sacerdoti Coen, C.: On the relative usefulness of fireballs. In: LICS 2015. IEEE (2015). https:\/\/doi.org\/10.1109\/LICS.2015.23","DOI":"10.1109\/LICS.2015.23"},{"key":"13_CR13","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Sacerdoti Coen, C.: On the value of variables. Inf. Comput. 255, 224\u2013242 (2017). https:\/\/doi.org\/10.1016\/j.ic.2017.01.003","DOI":"10.1016\/j.ic.2017.01.003"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"Biernacka, M., Biernacki, D., Charatonik, W., Drab, T.: An abstract machine for strong call by value. In: APLAS 2020 (2020). https:\/\/doi.org\/10.1007\/978-3-030-64437-6_8","DOI":"10.1007\/978-3-030-64437-6_8"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Biernacka, M., Charatonik, W., Drab, T.: A derived reasonable abstract machine for strong call by value. In: PPDP 2021. ACM (2021). https:\/\/doi.org\/10.1145\/3479394.3479401","DOI":"10.1145\/3479394.3479401"},{"key":"13_CR16","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzx018","author":"A Bucciarelli","year":"2017","unstructured":"Bucciarelli, A., Kesner, D., Ventura, D.: Non-idempotent intersection types for the lambda-calculus. Log. J. IGPL (2017). https:\/\/doi.org\/10.1093\/jigpal\/jzx018","journal-title":"Log. J. IGPL"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-54830-7_7","volume-title":"Foundations of Software Science and Computation Structures","author":"A Carraro","year":"2014","unstructured":"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\u2013118. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54830-7_7"},{"key":"13_CR18","volume-title":"S\u00e9mantiques de la logique lin\u00e9aire et temps de calcul","author":"D de Carvalho","year":"2007","unstructured":"de Carvalho, D.: S\u00e9mantiques de la logique lin\u00e9aire et temps de calcul. Universit\u00e9 Aix-Marseille II, Th\u00e8se de doctorat (2007)"},{"issue":"7","key":"13_CR19","doi-asserted-by":"publisher","first-page":"1169","DOI":"10.1017\/S0960129516000396","volume":"28","author":"D de Carvalho","year":"2018","unstructured":"de Carvalho, D.: Execution time of $$\\lambda $$-terms via denotational semantics and intersection types. Math. Str. Comput. Sci. 28(7), 1169\u20131203 (2018). https:\/\/doi.org\/10.1017\/S0960129516000396","journal-title":"Math. Str. Comput. Sci."},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"de Carvalho, D., Pagani, M., Tortora de Falco, L.: A semantic measure of the execution time in linear logic. Theor. Comput. Sci. 412(20), 1884\u20131902 (2011). https:\/\/doi.org\/10.1016\/j.tcs.2010.12.017","DOI":"10.1016\/j.tcs.2010.12.017"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Curien, P., Herbelin, H.: The duality of computation. In: ICFP 2000 (2000). https:\/\/doi.org\/10.1145\/351240.351262","DOI":"10.1145\/351240.351262"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"Dal Lago, U., Martini, S.: The weak lambda calculus as a reasonable machine. Theor. Comput. Sci. 398 (2008). https:\/\/doi.org\/10.1016\/j.tcs.2008.01.044","DOI":"10.1016\/j.tcs.2008.01.044"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-642-35722-0_12","volume-title":"Logical Foundations of Computer Science","author":"A D\u00edaz-Caro","year":"2013","unstructured":"D\u00edaz-Caro, A., Manzonetto, G., Pagani, M.: Call-by-value non-determinism in a linear logic type discipline. In: Artemov, S., Nerode, A. (eds.) LFCS 2013. LNCS, vol. 7734, pp. 164\u2013178. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35722-0_12"},{"issue":"6","key":"13_CR24","doi-asserted-by":"publisher","first-page":"1109","DOI":"10.1093\/logcom\/exm037","volume":"17","author":"R Dyckhoff","year":"2007","unstructured":"Dyckhoff, R., Lengrand, S.: Call-by-Value lambda-calculus and LJQ. J. Log. Comput. 17(6), 1109\u20131134 (2007). https:\/\/doi.org\/10.1093\/logcom\/exm037","journal-title":"J. Log. Comput."},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Ehrhard, T.: Collapsing non-idempotent intersection types. In: CSL 2012, pp. 259\u2013273. Schloss Dagstuhl (2012). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2012.259","DOI":"10.4230\/LIPIcs.CSL.2012.259"},{"key":"13_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"JY Girard","year":"1987","unstructured":"Girard, J.Y.: Linear Logic. Theore. Comput. Sci. 50, 1\u2013102 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4","journal-title":"Theore. Comput. Sci."},{"key":"13_CR27","doi-asserted-by":"publisher","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: ICFP 2002, pp. 235\u2013246. ACM (2002). https:\/\/doi.org\/10.1145\/581478.581501","DOI":"10.1145\/581478.581501"},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"Guerrieri, G.: Towards a semantic measure of the execution time in call-by-value $$\\lambda $$-calculus. In: DCM\/ITRS 2018 (2019). https:\/\/doi.org\/10.4204\/EPTCS.293.5","DOI":"10.4204\/EPTCS.293.5"},{"key":"13_CR29","doi-asserted-by":"publisher","unstructured":"Guerrieri, G., Paolini, L., Ronchi Della Rocca, S.: Standardization and conservativity of a refined call-by-value lambda-calculus. Log. Methods Comput. Sci. 13(4) (2017). https:\/\/doi.org\/10.23638\/LMCS-13(4:29)2017","DOI":"10.23638\/LMCS-13(4:29)2017"},{"key":"13_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-02273-9_12","volume-title":"Typed Lambda Calculi and Applications","author":"H Herbelin","year":"2009","unstructured":"Herbelin, H., Zimmermann, S.: An operational account of call-by-value minimal and classical $$\\lambda $$-calculus in \u201cNatural Deduction\u2019\u2019 form. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 142\u2013156. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02273-9_12"},{"key":"13_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-662-44602-7_23","volume-title":"Theoretical Computer Science","author":"D Kesner","year":"2014","unstructured":"Kesner, D., Ventura, D.: Quantitative types for the linear substitution calculus. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 296\u2013310. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44602-7_23"},{"key":"13_CR32","volume-title":"Lambda-Calculus, Types and Models","author":"J Krivine","year":"1993","unstructured":"Krivine, J.: Lambda-Calculus, Types and Models. Ellis Horwood, New York (1993)"},{"issue":"2","key":"13_CR33","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/S0890-5401(03)00088-9","volume":"185","author":"PB Levy","year":"2003","unstructured":"Levy, P.B., Power, J., Thielecke, H.: Modelling environments in call-by-value programming languages. Inf. Comput. 185(2), 182\u2013210 (2003). https:\/\/doi.org\/10.1016\/S0890-5401(03)00088-9","journal-title":"Inf. Comput."},{"issue":"1\u20132","key":"13_CR34","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/S0304-3975(98)00358-2","volume":"228","author":"J Maraist","year":"1999","unstructured":"Maraist, J., Odersky, M., Turner, D.N., Wadler, P.: Call-by-name, call-by-value, call-by-need and the linear $$\\lambda $$-calculus. Theor. Comput. Sci. 228(1\u20132), 175\u2013210 (1999). https:\/\/doi.org\/10.1016\/S0304-3975(98)00358-2","journal-title":"Theor. Comput. Sci."},{"key":"13_CR35","doi-asserted-by":"publisher","unstructured":"Mazza, D., Pellissier, L., Vial, P.: Polyadic approximations, fibrations and intersection types. Proc. ACM Program. Lang. 2(POPL), 6:1\u20136:28 (2018). https:\/\/doi.org\/10.1145\/3158094","DOI":"10.1145\/3158094"},{"key":"13_CR36","unstructured":"Moggi, E.: Computational $$\\lambda $$-Calculus and Monads. LFCS report ECS-LFCS-88-66, University of Edinburgh (1988). http:\/\/www.lfcs.inf.ed.ac.uk\/reports\/88\/ECS-LFCS-88-66\/ECS-LFCS-88-66.pdf"},{"key":"13_CR37","doi-asserted-by":"publisher","unstructured":"Moggi, E.: Computational $$\\lambda $$-calculus and monads. In: LICS 1989. IEEE Computer Society (1989). https:\/\/doi.org\/10.1109\/LICS.1989.39155","DOI":"10.1109\/LICS.1989.39155"},{"key":"13_CR38","doi-asserted-by":"publisher","unstructured":"Paolini, L.: Call-by-value separability and computability. In: ICTCS 2001 (2001). https:\/\/doi.org\/10.1007\/3-540-45446-2_5","DOI":"10.1007\/3-540-45446-2_5"},{"key":"13_CR39","doi-asserted-by":"publisher","unstructured":"Paolini, L., Ronchi Della Rocca, S.: Call-by-value solvability. RAIRO Theor. Inf. Appl. 33(6), 507\u2013534 (1999). https:\/\/doi.org\/10.1051\/ita:1999130","DOI":"10.1051\/ita:1999130"},{"key":"13_CR40","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1","author":"GD Plotkin","year":"1975","unstructured":"Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theore. Comput. Sci. (1975). https:\/\/doi.org\/10.1016\/0304-3975(75)90017-1","journal-title":"Theore. Comput. Sci."},{"key":"13_CR41","doi-asserted-by":"publisher","unstructured":"Ronchi Della Rocca, S., Paolini, L.: The parametric $${\\lambda }$$-calculus - a metamodel for computation. In: Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-662-10394-4","DOI":"10.1007\/978-3-662-10394-4"},{"issue":"3\u20134","key":"13_CR42","first-page":"289","volume":"6","author":"A Sabry","year":"1993","unstructured":"Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. LISP Symb. Comput. 6(3\u20134), 289\u2013360 (1993)","journal-title":"LISP Symb. Comput."},{"issue":"6","key":"13_CR43","doi-asserted-by":"publisher","first-page":"916","DOI":"10.1145\/267959.269968","volume":"19","author":"A Sabry","year":"1997","unstructured":"Sabry, A., Wadler, P.: A reflection on call-by-value. ACM Trans. Program. Lang. Syst. 19(6), 916\u2013941 (1997). https:\/\/doi.org\/10.1145\/267959.269968","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR44","unstructured":"Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press (2003)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2023"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-47963-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T21:42:39Z","timestamp":1700689359000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-47963-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031479625","9783031479632"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-47963-2_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"23 November 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lima","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Peru","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 December 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 December 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2023.compsust.utec.edu.pe\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}