{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T12:12:36Z","timestamp":1787314356834,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030719944","type":"print"},{"value":"9783030719951","type":"electronic"}],"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>\n                  <jats:p>\n                    We introduce a generalization of Girard et al.\u2019s  called  (and its affine variant ). It is designed to capture the core mechanism of dependency in , while it is also able to separate complexity aspects of . The main feature of  is to adopt a multi-object pseudo-semiring as a grading system of the !-modality. We analyze the complexity of cut-elimination in , and give a translation from  with constraints to  with positivity axiom. We then introduce\n                    <jats:italic>indexed linear exponential comonads<\/jats:italic>\n                    (\n                    <jats:italic>ILEC<\/jats:italic>\n                    for short) as a categorical structure for interpreting the\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$${!}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mo>!<\/mml:mo>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -modality of . We give an elementary example of ILEC using folding product, and a technique to modify ILECs with symmetric monoidal comonads. We then consider a semantics of  using the folding product on the category of assemblies of a BCI-algebra, and relate the semantics with the realizability category studied by Hofmann, Scott and Dal Lago.\n                  <\/jats:p>","DOI":"10.1007\/978-3-030-71995-1_12","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T13:03:39Z","timestamp":1616418219000},"page":"226-246","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Generalized Bounded Linear Logic and its Categorical Semantics"],"prefix":"10.1007","author":[{"given":"Y\u014dji","family":"Fukihara","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7529-5489","authenticated-orcid":false,"given":"Shin-ya","family":"Katsumata","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Abel, A., Bernardy, J.P.: A unified view of modalities in type systems. Proc. ACM Program. Lang. 4(ICFP) (Aug 2020). https:\/\/doi.org\/10.1145\/3408972","DOI":"10.1145\/3408972"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Abramsky, S., Lenisa, M.: Linear realizability and full completeness for typed lambda-calculi. Ann. Pure Appl. Log. 134(2-3), 122\u2013168 (2005). https:\/\/doi.org\/10.1016\/j.apal.2004.08.003","DOI":"10.1016\/j.apal.2004.08.003"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"de\u00a0Amorim, A.A., Gaboardi, M., Hsu, J., Katsumata, S., Cherigui, I.: A semantic account of metric preservation. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 545\u2013556. ACM (2017). https:\/\/doi.org\/10.1145\/3009837, http:\/\/dl.acm.org\/citation.cfm?id=3009890","DOI":"10.1145\/3009837"},{"key":"12_CR4","doi-asserted-by":"publisher","unstructured":"Atkey, R.: Syntax and semantics of quantitative type theory. In: Dawar, A.,Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposiumon Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 56\u201365. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209189","DOI":"10.1145\/3209108.3209189"},{"key":"12_CR5","unstructured":"Breuvart, F.: Dissecting Denotational Semantics: From the Well-established$$\\,\\, \\cal{H}^*$$ to the More Recent Quantitative Coeffects. Ph.D. thesis, Universit\u00e9 Paris Diderot (2015), https:\/\/lipn.univ-paris13.fr\/~breuvart\/These_breuvart.pdf"},{"key":"12_CR6","unstructured":"Breuvart, F., Pagani, M.: Modelling coeffects in the relational semantics of linear logic. In: Kreutzer [23], pp. 567\u2013581, http:\/\/www.dagstuhl.de\/dagpub\/978-3-939897-90-3"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Brunel, A., Gaboardi, M., Mazza, D., Zdancewic, S.: A core quantitative coeffect calculus. In: Shao, Z. (ed.) Programming Languages and Systems. pp. 351\u2013370. Springer Berlin Heidelberg, Berlin, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_19","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Bucciarelli, A., Ehrhard, T.: On phase semantics and denotational semantics in multiplicative-additive linear logic. Ann. Pure Appl. Log. 102(3), 247\u2013282 (2000). https:\/\/doi.org\/10.1016\/S0168-0072(99)00040-8","DOI":"10.1016\/S0168-0072(99)00040-8"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Bucciarelli, A., Ehrhard, T.: On phase semantics and denotational semantics: the exponentials. Annals of Pure and Applied Logic 109(3), 205 \u2013241 (2001). https:\/\/doi.org\/10.1016\/S0168-0072(00)00056-7, http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0168007200000567","DOI":"10.1016\/S0168-0072(00)00056-7"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Dal\u00a0Lago, U., Hofmann, M.: Bounded linear logic, revisited. In: Curien, P.L.(ed.) Typed Lambda Calculi and Applications. pp. 80\u201394. Springer Berlin Heidelberg, Berlin, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02273-9_8","DOI":"10.1007\/978-3-642-02273-9_8"},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Fujii, S., Katsumata, S., Melli\u00e8s, P.: Towards a formal theory of graded monads. In: Jacobs, B., L\u00f6ding, C. (eds.) Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS2016, 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.\u00a09634, pp. 513\u2013530. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49630-5_30","DOI":"10.1007\/978-3-662-49630-5_30"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Gaboardi, M., Haeberlen, A., Hsu, J., Narayan, A., Pierce, B.C.: Linear dependent types for differential privacy. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy - January 23 - 25, 2013. pp. 357\u2013370. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429113, http:\/\/dl.acm.org\/citation.cfm?id=2429069","DOI":"10.1145\/2429069.2429113"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Gaboardi, M., Katsumata, S., Orchard, D., Breuvart, F., Uustalu, T.: Combining effects and coeffects via grading. SIGPLAN Not. 51(9), 476\u2013489 (Sep 2016). https:\/\/doi.org\/10.1145\/3022670.2951939","DOI":"10.1145\/3022670.2951939"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Ghica, D.R., Smith, A.I.: Bounded linear types in a resource semiring. In: Shao, Z. (ed.) Programming Languages and Systems. pp. 331\u2013350. SpringerBerlin Heidelberg, Berlin, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_18","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"12_CR15","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":"12_CR16","doi-asserted-by":"publisher","unstructured":"Girard, J., Scedrov, A., Scott, P.J.: Bounded linear logic: A modular approach to polynomial-time computability. Theor. Comput. Sci. 97(1), 1\u201366 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90386-T","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"Grellois, C., Melli\u00e8s, P.: An infinitary model of linear logic. In:Pitts, A.M. (ed.) Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. Lecture Notes in Computer Science,vol.\u00a09034, pp. 41\u201355. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46678-0_3","DOI":"10.1007\/978-3-662-46678-0_3"},{"key":"12_CR18","unstructured":"Grellois, C., Melli\u00e8s, P.: Relational semantics of linear logic and higher-order model checking. In: Kreutzer [23], pp. 260\u2013276, http:\/\/www.dagstuhl.de\/dagpub\/978-3-939897-90-3"},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Hofmann, M., Scott, P.J.: Realizability models for bll-like languages. Theor. Comput. Sci. 318(1-2), 121\u2013137 (2004). https:\/\/doi.org\/10.1016\/j.tcs.2003.10.019","DOI":"10.1016\/j.tcs.2003.10.019"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Hoshino, N.: Linear realizability. In: Duparc, J., Henzinger, T.A. (eds.) Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings. Lecture Notes in Computer Science, vol.\u00a04646, pp. 420\u2013434.Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-74915-8_32","DOI":"10.1007\/978-3-540-74915-8_32"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Hyland, M., Power, J.: Pseudo-commutative monads and pseudo-closed 2-categories. Journal of Pure and Applied Algebra 175(1), 141 \u2013 185 (2002). https:\/\/doi.org\/10.1016\/S0022-4049(02)00133-0, http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0022404902001330,special Volume celebrating the 70th birthday of Professor Max Kelly","DOI":"10.1016\/S0022-4049(02)00133-0"},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"Katsumata, S.: A double category theoretic analysis of graded linear exponential comonads. In: Baier, C., Dal\u00a0Lago, U. (eds.) Foundations of Software Science and Computation Structures. pp. 110\u2013127. Springer International Publishing, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89366-2_6","DOI":"10.1007\/978-3-319-89366-2_6"},{"key":"12_CR23","unstructured":"Kreutzer, S. (ed.): 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, LIPIcs, vol.\u00a041. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2015), http:\/\/www.dagstuhl.de\/dagpub\/978-3-939897-90-3"},{"key":"12_CR24","doi-asserted-by":"publisher","unstructured":"Lago, U.D., Gaboardi, M.: Linear dependent types and relative completeness. In: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada. pp. 133\u2013142. IEEE Computer Society (2011). https:\/\/doi.org\/10.1109\/LICS.2011.22, https:\/\/ieeexplore.ieee.org\/xpl\/conhome\/5968099\/proceeding","DOI":"10.1109\/LICS.2011.22"},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"McBride, C.: I got plenty o\u2019 nuttin\u2019. In: Lindley, S., McBride, C., Trinder,P.W., Sannella, D. (eds.) A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol.\u00a09600, pp. 207\u2013233. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-30936-1_12","DOI":"10.1007\/978-3-319-30936-1_12"},{"key":"12_CR26","doi-asserted-by":"publisher","unstructured":"Orchard, D., Liepelt, V.B., Eades\u00a0III, H.: Quantitative program reasoning with graded modal types. Proc. ACM Program. Lang. 3(ICFP) (Jul 2019). https:\/\/doi.org\/10.1145\/3341714","DOI":"10.1145\/3341714"},{"key":"12_CR27","doi-asserted-by":"publisher","unstructured":"Orchard, D., Wadler, P., Eades, H.: Unifying graded and parameterised monads. Electronic Proceedings in Theoretical Computer Science 317, 18\u201338 (May 2020). https:\/\/doi.org\/10.4204\/eptcs.317.2","DOI":"10.4204\/eptcs.317.2"},{"key":"12_CR28","doi-asserted-by":"publisher","unstructured":"Petricek, T., Orchard, D., Mycroft, A.: Coeffects: Unified static analysis of context-dependence. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) Automata, Languages, and Programming. pp. 385\u2013397. Springer Berlin Heidelberg, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39212-2_35","DOI":"10.1007\/978-3-642-39212-2_35"},{"key":"12_CR29","doi-asserted-by":"publisher","unstructured":"Reed, J., Pierce, B.C.: Distance makes the types grow stronger: a calculus for differential privacy. In: Hudak, P., Weirich, S. (eds.) Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010. pp. 157\u2013168. ACM (2010). https:\/\/doi.org\/10.1145\/1863543.1863568","DOI":"10.1145\/1863543.1863568"},{"key":"12_CR30","doi-asserted-by":"publisher","unstructured":"Sch\u00f6pp, U.: Computation-by-interaction with effects. In: Yang, H. (ed.)Programming Languages and Systems. pp. 305\u2013321. Springer Berlin Heidelberg, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25318-8_23","DOI":"10.1007\/978-3-642-25318-8_23"}],"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_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T13:08:04Z","timestamp":1616418484000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-71995-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030719944","9783030719951"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-71995-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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)"}}]}}