{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T16:10:54Z","timestamp":1746115854268,"version":"3.40.4"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031908965"},{"type":"electronic","value":"9783031908972"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"Abstract<\/jats:title>\n The two Girard translations provide two different means of obtaining embeddings of Intuitionistic Logic into Linear Logic, corresponding to different lambda-calculus calling mechanisms. The translations, mapping \n \n $$A\\rightarrow B$$<\/jats:tex-math>\n \n \n A<\/mml:mi>\n \u2192<\/mml:mo>\n B<\/mml:mi>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> respectively to \n \n $${!}{A}\\multimap B$$<\/jats:tex-math>\n \n \n !<\/mml:mo>\n A<\/mml:mi>\n \u22b8<\/mml:mo>\n B<\/mml:mi>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> and \n \n $${!}{(A\\multimap B)}$$<\/jats:tex-math>\n \n \n !<\/mml:mo>\n \n (<\/mml:mo>\n A<\/mml:mi>\n \u22b8<\/mml:mo>\n B<\/mml:mi>\n )<\/mml:mo>\n <\/mml:mrow>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, have been shown to correspond respectively to call-by-name and call-by-value.<\/jats:p>\n In this work, we split the of-course<\/jats:italic> modality of linear logic into two modalities, written \u201c\n \n $${!} $$<\/jats:tex-math>\n \n !<\/mml:mo>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\u201d and \u201c\n \n $$\\bullet $$<\/jats:tex-math>\n \n \u2219<\/mml:mo>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\u201d. Intuitively, the modality \u201c\n \n $${!} $$<\/jats:tex-math>\n \n !<\/mml:mo>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\u201d specifies a subproof that can be duplicated and erased, but may not necessarily be \u201caccessed\u201d, i.e.<\/jats:italic> interacted with, while the combined modality \u201c\n \n $${!}{\\bullet }$$<\/jats:tex-math>\n \n \n !<\/mml:mo>\n \u2219<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\u201d specifies a subproof that can moreover be accessed. The resulting system, called \n \n $$\\textsf{MSCLL}$$<\/jats:tex-math>\n \n MSCLL<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, enjoys cut-elimination and is conservative over \n \n $$\\textsf{MELL}$$<\/jats:tex-math>\n \n MELL<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>.<\/jats:p>\n We study how restricting access to subproofs provides ways to control sharing<\/jats:italic> in evaluation strategies. For this, we introduce a term-assignment for an intuitionistic fragment of \n \n $$\\textsf{MSCLL}$$<\/jats:tex-math>\n \n MSCLL<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, called the \n \n $$\\lambda ^{{!}{\\bullet }}$$<\/jats:tex-math>\n \n \n \u03bb<\/mml:mi>\n \n !<\/mml:mo>\n \u2219<\/mml:mo>\n <\/mml:mrow>\n <\/mml:msup>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>-calculus, which we show to\u00a0enjoy subject reduction, confluence, and strong normalization of the simply typed fragment. We propose three sound and complete translations that respectively simulate call-by-name, call-by-value, and a variant of call-by-name that shares<\/jats:italic> the evaluation of its arguments (similarly as in call-by-need). The translations are extended to simulate the Bang-calculus, as well as\u00a0weak reduction strategies.<\/jats:p>","DOI":"10.1007\/978-3-031-90897-2_14","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:55Z","timestamp":1746001075000},"page":"287-307","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Sharing and Linear Logic with Restricted Access"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-2494-3345","authenticated-orcid":false,"given":"Pablo","family":"Barenbaum","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1856-2856","authenticated-orcid":false,"given":"Eduardo","family":"Bonelli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","unstructured":"Accattoli, B.: An abstract factorization theorem for explicit substitutions. In: Tiwari, A. (ed.) 23rd International Conference on Rewriting Techniques and Applications (RTA\u201912) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan. LIPIcs, vol.\u00a015, pp. 6\u201321. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2012). https:\/\/doi.org\/10.4230\/LIPICS.RTA.2012.6, https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2012.6","DOI":"10.4230\/LIPICS.RTA.2012.6"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Accattoli, B.: Proof nets and the linear substitution calculus. In: Fischer, B., Uustalu, T. (eds.) Theoretical Aspects of Computing - ICTAC 2018 - 15th International Colloquium, Stellenbosch, South Africa, October 16-19, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11187, pp. 37\u201361. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-02508-3_3, https:\/\/doi.org\/10.1007\/978-3-030-02508-3_3","DOI":"10.1007\/978-3-030-02508-3_3"},{"key":"14_CR3","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C.: A nonstandard standardization theorem. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914, San Diego, CA, USA, January 20-21, 2014. pp. 659\u2013670. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535886, https:\/\/doi.org\/10.1145\/2535838.2535886","DOI":"10.1145\/2535838.2535886"},{"key":"14_CR4","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Kesner, D.: The structural lambda-calculus. In: Dawar, A., Veith, H. (eds.) Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings. Lecture Notes in Computer Science, vol.\u00a06247, pp. 381\u2013395. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-15205-4_30, https:\/\/doi.org\/10.1007\/978-3-642-15205-4_30","DOI":"10.1007\/978-3-642-15205-4_30"},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Paolini, L.: Call-by-value solvability, revisited. In: Schrijvers, T., Thiemann, P. (eds.) Functional and Logic Programming - 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings. Lecture Notes in Computer Science, vol.\u00a07294, pp. 4\u201316. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-29822-6_4, https:\/\/doi.org\/10.1007\/978-3-642-29822-6_4","DOI":"10.1007\/978-3-642-29822-6_4"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Ariola, Z.M., Felleisen, M., Maraist, J., Odersky, M., Wadler, P.: A call-by-need lambda calculus. In: Conference Record of POPL\u201995: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995. pp. 233\u2013246 (1995)","DOI":"10.1145\/199448.199507"},{"key":"14_CR7","unstructured":"Arrial, V.: A deeper study of $$\\lambda !$$-calculus simulations. In: Fuhs, C. (ed.) Proceedings of the 11th International Workshop on Higher-Order Rewriting (HOR 2023) (July 2023)"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Balabonski, T., Barenbaum, P., Bonelli, E., Kesner, D.: Foundations of strong call by need. Proc. ACM Program. Lang. 1(ICFP), 20:1\u201320:29 (2017). https:\/\/doi.org\/10.1145\/3110264, https:\/\/doi.org\/10.1145\/3110264","DOI":"10.1145\/3110264"},{"key":"14_CR9","doi-asserted-by":"publisher","unstructured":"Balabonski, T., Lanco, A., Melquiond, G.: A strong call-by-need calculus. Log. Methods Comput. Sci. 19(1) (2023). https:\/\/doi.org\/10.46298\/LMCS-19(1:21)2023, https:\/\/doi.org\/10.46298\/lmcs-19(1:21)2023","DOI":"10.46298\/LMCS-19(1:21)2023"},{"key":"14_CR10","doi-asserted-by":"publisher","unstructured":"Barenbaum, P., Bonelli, E.: Sharing and linear logic with restricted access (extended version). CoRR abs\/2501.16576 (2025). https:\/\/doi.org\/10.48550\/ARXIV.2501.16576, https:\/\/doi.org\/10.48550\/arXiv.2501.16576","DOI":"10.48550\/ARXIV.2501.16576"},{"key":"14_CR11","unstructured":"Barendregt, H.P.: The lambda calculus - its syntax and semantics, Studies in logic and the foundations of mathematics, vol.\u00a0103. North-Holland (1985)"},{"key":"14_CR12","doi-asserted-by":"publisher","unstructured":"Bucciarelli, A., Kesner, D., R\u00edos, A., Viso, A.: The bang calculus revisited. In: Nakano, K., Sagonas, K. (eds.) Functional and Logic Programming - 15th International Symposium, FLOPS 2020, Akita, Japan, September 14-16, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12073, pp. 13\u201332. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-59025-3_2, https:\/\/doi.org\/10.1007\/978-3-030-59025-3_2","DOI":"10.1007\/978-3-030-59025-3_2"},{"key":"14_CR13","doi-asserted-by":"publisher","unstructured":"Bucciarelli, A., Kesner, D., R\u00edos, A., Viso, A.: The bang calculus revisited. Inf. Comput. 293, 105047 (2023). https:\/\/doi.org\/10.1016\/J.IC.2023.105047, https:\/\/doi.org\/10.1016\/j.ic.2023.105047","DOI":"10.1016\/J.IC.2023.105047"},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Ehrhard, T.: Call-by-push-value from a linear logic point of view. In: Thiemann, P. (ed.) 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. Lecture Notes in Computer Science, vol.\u00a09632, pp. 202\u2013228. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_9, https:\/\/doi.org\/10.1007\/978-3-662-49498-1_9","DOI":"10.1007\/978-3-662-49498-1_9"},{"key":"14_CR15","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: Cheney, J., Vidal, G. (eds.) Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016. pp. 174\u2013187. ACM (2016). https:\/\/doi.org\/10.1145\/2967973.2968608, https:\/\/doi.org\/10.1145\/2967973.2968608","DOI":"10.1145\/2967973.2968608"},{"key":"14_CR16","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, https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"14_CR17","doi-asserted-by":"publisher","unstructured":"Guerrieri, G., Manzonetto, G.: The bang calculus and the two girard\u2019s translations. In: Ehrhard, T., Fern\u00e1ndez, M., de\u00a0Paiva, V., de\u00a0Falco, L.T. (eds.) Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, Oxford, UK, 7-8 July 2018. EPTCS, vol.\u00a0292, pp. 15\u201330 (2018). https:\/\/doi.org\/10.4204\/EPTCS.292.2, https:\/\/doi.org\/10.4204\/EPTCS.292.2","DOI":"10.4204\/EPTCS.292.2"},{"key":"14_CR18","doi-asserted-by":"publisher","unstructured":"Herbelin, H., Zimmermann, S.: An operational account of call-by-value minimal and classical lambda-calculus in \"natural deduction\" form. In: Curien, P. (ed.) Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05608, pp. 142\u2013156. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02273-9_12, https:\/\/doi.org\/10.1007\/978-3-642-02273-9_12","DOI":"10.1007\/978-3-642-02273-9_12"},{"key":"14_CR19","doi-asserted-by":"publisher","unstructured":"Kesner, D., Conch\u00fair, S.\u00d3.: Milner\u2019s lambda-calculus with partial substitutions. CoRR abs\/2312.13270 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2312.13270, https:\/\/doi.org\/10.48550\/arXiv.2312.13270","DOI":"10.48550\/ARXIV.2312.13270"},{"key":"14_CR20","unstructured":"Levy, P.B.: Call-By-Push-Value: A Functional\/Imperative Synthesis, Semantics Structures in Computation, vol.\u00a02. Springer (2004)"},{"key":"14_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, https:\/\/doi.org\/10.1007\/s10990-006-0480-6","DOI":"10.1007\/S10990-006-0480-6"},{"key":"14_CR22","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, https:\/\/doi.org\/10.1016\/S0304-3975(98)00358-2","DOI":"10.1016\/S0304-3975(98)00358-2"},{"key":"14_CR23","unstructured":"Melli\u00e8s, P.A.: Description abstraite des syst\u00e9mes de r\u00e9\u00e9criture. Ph.D. thesis, Universit\u00e9 Paris VII (1996)"},{"key":"14_CR24","doi-asserted-by":"publisher","unstructured":"Milner, R.: Local bigraphs and confluence: Two conjectures: (extended abstract). In: Amadio, R.M., Phillips, I. (eds.) Proceedings of the 13th International Workshop on Expressiveness in Concurrency, EXPRESS 2006, Bonn, Germany, August 26, 2006. Electronic Notes in Theoretical Computer Science, vol.\u00a0175, pp. 65\u201373. Elsevier (2006). https:\/\/doi.org\/10.1016\/J.ENTCS.2006.07.035, https:\/\/doi.org\/10.1016\/j.entcs.2006.07.035","DOI":"10.1016\/J.ENTCS.2006.07.035"},{"key":"14_CR25","doi-asserted-by":"publisher","unstructured":"Nigam, V., Miller, D.: Algorithmic specifications in linear logic with subexponentials. In: Porto, A., L\u00f3pez-Fraguas, F.J. (eds.) Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal. pp. 129\u2013140. ACM (2009). https:\/\/doi.org\/10.1145\/1599410.1599427, https:\/\/doi.org\/10.1145\/1599410.1599427","DOI":"10.1145\/1599410.1599427"},{"key":"14_CR26","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, https:\/\/doi.org\/10.1016\/0304-3975(75)90017-1","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"14_CR27","doi-asserted-by":"publisher","unstructured":"Santo, J.E., Pinto, L., Uustalu, T.: Modal embeddings and calling paradigms. In: Geuvers, H. (ed.) 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany. LIPIcs, vol.\u00a0131, pp. 18:1\u201318:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPICS.FSCD.2019.18, https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.18","DOI":"10.4230\/LIPICS.FSCD.2019.18"},{"key":"14_CR28","unstructured":"Wadsworth, C.P.: Semantics and pragmatics of the lambda-calculus. Ph.D. thesis, Oxford University (1971)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90897-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:18:03Z","timestamp":1746001083000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90897-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031908965","9783031908972"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90897-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","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":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}