{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:12:26Z","timestamp":1762459946756,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030719944"},{"type":"electronic","value":"9783030719951"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In each variant of the <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03bb<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus, factorization and normalization are two key properties that show how results are computed. Instead of proving factorization\/normalization for the call-by-name (CbN) and call-by-value (CbV) variants separately, we prove them only once, for the bang calculus (an extension of the <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03bb<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus inspired by linear logic and subsuming CbN and CbV), and then we transfer the result via translations, obtaining factorization\/normalization for CbN and CbV.<\/jats:p><jats:p>The approach is robust: it still holds when extending the calculi with operators and extra rules to model some additional computational features.<\/jats:p>","DOI":"10.1007\/978-3-030-71995-1_11","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T17:03:39Z","timestamp":1616432619000},"page":"205-225","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic"],"prefix":"10.1007","author":[{"given":"Claudia","family":"Faggian","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0469-4279","authenticated-orcid":false,"given":"Giulio","family":"Guerrieri","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","unstructured":"Accattoli, B.: An Abstract Factorization Theorem for Explicit Substitutions. In: 23rd International Conference on Rewriting Techniques and Applications (RTA\u201912). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a015, pp. 6\u201321. Schloss Dagstuhl (2012). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2012.6","DOI":"10.4230\/LIPIcs.RTA.2012.6"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Faggian, C., Guerrieri, G.: Factorization and normalization, essentially. In: Programming Languages and Systems - 17th Asian Symposium, APLAS 2019. Lecture Notes in Computer Science, vol. 11893, pp. 159\u2013180. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-34175-6_9","DOI":"10.1007\/978-3-030-34175-6_9"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Faggian, C., Guerrieri, G.: Factorize factorization. In: 29th EACSL Annual Conference on Computer Science Logic, CSL 2021. LIPIcs, vol.\u00a0183, pp. 6:1\u20136:25. Schloss-Dagstuhl (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2021.6","DOI":"10.4230\/LIPIcs.CSL.2021.6"},{"key":"11_CR4","unstructured":"Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, vol.\u00a0103. North Holland (1984)"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Benton, P.N., Bierman, G.M., de\u00a0Paiva, V., Hyland, M.: A term calculus for intuitionistic linear logic. In: International Conference on Typed Lambda Calculi and Applications, TLCA \u201993. Lecture Notes in Computer Science, vol.\u00a0664, pp. 75\u201390. Springer (1993). https:\/\/doi.org\/10.1007\/BFb0037099","DOI":"10.1007\/BFb0037099"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Benton, P.N., Wadler, P.: Linear logic, monads and the lambda calculus. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, LICS 1996. pp. 420\u2013431. IEEE Computer Society (1996). https:\/\/doi.org\/10.1109\/LICS.1996.561458","DOI":"10.1109\/LICS.1996.561458"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Bucciarelli, A., Kesner, D., R\u00edos, A., Viso, A.: The bang calculus revisited. In: Functional and Logic Programming - 15th International Symposium, FLOPS 2020. Lecture Notes in Computer Science, vol. 12073, pp. 13\u201332. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-59025-3_2","DOI":"10.1007\/978-3-030-59025-3_2"},{"key":"11_CR8","doi-asserted-by":"publisher","unstructured":"de\u00a0Carvalho, 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":"11_CR9","doi-asserted-by":"publisher","unstructured":"Chouquet, J., Tasson, C.: Taylor expansion for Call-By-Push-Value. In: 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0152, pp. 16:1\u201316:16. Schloss Dagstuhl (2020). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2020.16","DOI":"10.4230\/LIPIcs.CSL.2020.16"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Ehrhard, T.: Call-by-push-value from a linear logic point of view. In: Programming Languages and Systems - 25th European Symposium on Programming (ESOP 2016). Lecture Notes in Computer Science, vol.\u00a09632, pp. 202\u2013228 (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_9","DOI":"10.1007\/978-3-662-49498-1_9"},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Ehrhard, T., Guerrieri, G.: The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016). pp. 174\u2013187. ACM (2016). https:\/\/doi.org\/10.1145\/2967973.2968608","DOI":"10.1145\/2967973.2968608"},{"key":"11_CR12","unstructured":"Faggian, C., Guerrieri, G.: Factorization in call-by-name and call-by-value calculi via linear logic (long version). CoRR abs\/2101.08364 (2021), https:\/\/arxiv.org\/abs\/2101.08364"},{"key":"11_CR13","doi-asserted-by":"publisher","unstructured":"Faggian, C., Ronchi Della Rocca, S.: Lambda calculus and probabilistic computation. In: 34th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2019. pp. 1\u201313. IEEE (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785699","DOI":"10.1109\/LICS.2019.8785699"},{"key":"11_CR14","doi-asserted-by":"publisher","unstructured":"Girard, J.: Linear logic. Theor. Comput. Sci. 50, 1\u2013102 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Guerrieri, G., Manzonetto, G.: The bang calculus and the two Girard\u2019s translations. In: Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity-TLLA 2018). EPTCS, vol.\u00a0292, pp. 15\u201330 (2019). https:\/\/doi.org\/10.4204\/EPTCS.292.2","DOI":"10.4204\/EPTCS.292.2"},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Guerrieri, G., Olimpieri, F.: Categorifying non-idempotent intersection types. In: 29th EACSL Annual Conference on Computer Science Logic, CSL 2021. LIPIcs, vol.\u00a0183, pp. 25:1\u201325:24. Schloss Dagstuhl (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2021.25","DOI":"10.4230\/LIPIcs.CSL.2021.25"},{"key":"11_CR17","unstructured":"Hindley, J.R.: The Church-Rosser Property and a Result in Combinatory Logic. Ph.D. thesis, University of Newcastle-upon-Tyne (1964)"},{"key":"11_CR18","unstructured":"Hindley, J.R., Seldin, J.P.: Introduction to Combinators and Lambda-Calculus. Cambridge University Press (1986)"},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"Hirokawa, N., Middeldorp, A., Moser, G.: Leftmost Outermost Revisited. In: 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a036, pp. 209\u2013222. Schloss Dagstuhl (2015). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2015.209","DOI":"10.4230\/LIPIcs.RTA.2015.209"},{"key":"11_CR20","doi-asserted-by":"publisher","unstructured":"Levy, P.B.: Call-by-push-value: A subsuming paradigm. In: Typed Lambda Calculi and Applications, 4th International Conference (TLCA\u201999). Lecture Notes in Computer Science, vol.\u00a01581, pp. 228\u2013242 (1999). https:\/\/doi.org\/10.1007\/3-540-48959-2_17","DOI":"10.1007\/3-540-48959-2_17"},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"Levy, P.B.: Call-by-push-value: Decomposing call-by-value and call-by-name. High. Order Symb. Comput. 19(4), 377\u2013414 (2006). https:\/\/doi.org\/10.1007\/s10990-006-0480-6","DOI":"10.1007\/s10990-006-0480-6"},{"key":"11_CR22","unstructured":"de\u2019 Liguoro, U.: Non-deterministic untyped $$\\lambda $$-calculus. A study about explicit non determinism in higher-order functional calculi. Ph.D. thesis, Universit\u00e0 di Roma La Sapienza (1991), http:\/\/www.di.unito.it\/~deligu\/papers\/UdLTesi.pdf"},{"key":"11_CR23","doi-asserted-by":"publisher","unstructured":"de\u2019 Liguoro, U., Piperno, A.: Non deterministic extensions of untyped lambda-calculus. Inf. Comput. 122(2), 149\u2013177 (1995). https:\/\/doi.org\/10.1006\/inco.1995.1145","DOI":"10.1006\/inco.1995.1145"},{"key":"11_CR24","doi-asserted-by":"publisher","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-2), 175\u2013210 (1999). https:\/\/doi.org\/10.1016\/S0304-3975(98)00358-2","DOI":"10.1016\/S0304-3975(98)00358-2"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Newman, M.: On theories with a combinatorial definition of equivalence. Annals of Mathematics 43(2) (1942)","DOI":"10.2307\/1968867"},{"key":"11_CR26","doi-asserted-by":"publisher","unstructured":"Pagani, M., Tranquilli, P.: The conservation theorem for differential nets. Math. Struct. Comput. Sci. 27(6), 939\u2013992 (2017). https:\/\/doi.org\/10.1017\/S0960129515000456","DOI":"10.1017\/S0960129515000456"},{"key":"11_CR27","doi-asserted-by":"publisher","unstructured":"Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125\u2013159 (1975). https:\/\/doi.org\/10.1016\/0304-3975(75)90017-1","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"11_CR28","unstructured":"Ronchi Della Rocca, S., Paolini, L.: The Parametric Lambda Calculus - A Metamodel for Computation. Texts in Theoretical Computer Science. An EATCS Series, Springer (2004)"},{"key":"11_CR29","doi-asserted-by":"publisher","unstructured":"Ronchi Della Rocca, S., Roversi, L.: Lambda calculus and intuitionistic linear logic. Stud Logica 59(3), 417\u2013448 (1997). https:\/\/doi.org\/10.1023\/A:1005092630115","DOI":"10.1023\/A:1005092630115"},{"key":"11_CR30","doi-asserted-by":"publisher","unstructured":"Santo, J.E., Pinto, L., Uustalu, T.: Modal embeddings and calling paradigms. In: 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019. LIPIcs, vol.\u00a0131, pp. 18:1\u201318:20. Schloss Dagstuhl (2019). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.18","DOI":"10.4230\/LIPIcs.FSCD.2019.18"},{"key":"11_CR31","doi-asserted-by":"publisher","unstructured":"Simpson, A.K.: Reduction in a linear lambda-calculus with applications to operational semantics. In: Term Rewriting and Applications, 16th International Conference (RTA 2005). Lecture Notes in Computer Science, vol.\u00a03467, pp. 219\u2013234 (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_17","DOI":"10.1007\/978-3-540-32033-3_17"},{"key":"11_CR32","doi-asserted-by":"publisher","unstructured":"Takahashi, M.: Parallel reductions in lambda-calculus. Inf. Comput. 118(1), 120\u2013127 (1995). https:\/\/doi.org\/10.1006\/inco.1995.1057","DOI":"10.1006\/inco.1995.1057"},{"key":"11_CR33","unstructured":"Terese: Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, vol.\u00a055. Cambridge University Press (2003)"},{"key":"11_CR34","doi-asserted-by":"publisher","unstructured":"Terui, K.: Light affine lambda calculus and polynomial time strong normalization. Archive for Mathematical Logic 46(3-4), 253\u2013280 (2007). https:\/\/doi.org\/10.1007\/s00153-007-0042-6","DOI":"10.1007\/s00153-007-0042-6"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-71995-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T17:05:52Z","timestamp":1616432752000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-71995-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030719944","9783030719951"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-71995-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FOSSACS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"88","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}