{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T18:42:14Z","timestamp":1757616134948,"version":"3.44.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030171261"},{"type":"electronic","value":"9783030171278"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T00:00:00Z","timestamp":1554422400000},"content-version":"vor","delay-in-days":94,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Commuting conversions of Linear Logic induce a notion of dependency between rules inside a proof derivation: a rule depends on a previous rule when they cannot be permuted using the conversions. We propose a new interpretation of proofs of Linear Logic as <jats:italic>causal invariants<\/jats:italic> which captures <jats:italic>exactly<\/jats:italic> this dependency. We represent causal invariants using game semantics based on general event structures, carving out, inside the model of [6], a submodel of causal invariants. This submodel supports an interpretation of unit-free Multiplicative Additive Linear Logic with MIX (MALL<jats:inline-formula>\n              <jats:tex-math>$$^-$$<\/jats:tex-math>\n            <\/jats:inline-formula>) which is (1) <jats:italic>fully complete<\/jats:italic>: every element of the model is the denotation of a proof and (2) <jats:italic>injective<\/jats:italic>: equality in the model characterises exactly commuting conversions of MALL<jats:inline-formula>\n              <jats:tex-math>$$^-$$<\/jats:tex-math>\n            <\/jats:inline-formula>. This improves over the standard fully complete game semantics model of MALL<jats:inline-formula>\n              <jats:tex-math>$$^-$$<\/jats:tex-math>\n            <\/jats:inline-formula>.<\/jats:p>","DOI":"10.1007\/978-3-030-17127-8_9","type":"book-chapter","created":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T11:11:46Z","timestamp":1554462706000},"page":"150-168","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Causality in Linear Logic"],"prefix":"10.1007","author":[{"given":"Simon","family":"Castellan","sequence":"first","affiliation":[]},{"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,4,5]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Melli\u00e9s, P.-A.: Concurrent games and full completeness. In: 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, 2\u20135 July 1999, pp. 431\u2013442 (1999). http:\/\/dx.doi.org\/10.1109\/LICS.1999.782638","DOI":"10.1109\/LICS.1999.782638"},{"key":"9_CR2","unstructured":"Baelde, D., Doumane, A., Saurin, A.: Infinitary proof theory: the multiplicative additive case. In: CSL. Leibniz International Proceedings in Informatics (LIPIcs), vol. 62, pp. 42:1\u201342:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2016)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-662-46678-0_28","volume-title":"Foundations of Software Science and Computation Structures","author":"M Bagnol","year":"2015","unstructured":"Bagnol, M., Doumane, A., Saurin, A.: On the dependencies of logical rules. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 436\u2013450. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46678-0_28"},{"issue":"1\u20133","key":"9_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.apal.2004.05.002","volume":"131","author":"R Blute","year":"2005","unstructured":"Blute, R., Hamano, M., Scott, P.J.: Softness of hypercoherences and MALL full completeness. Ann. Pure Appl. Logic 131(1\u20133), 1\u201363 (2005). https:\/\/doi.org\/10.1016\/j.apal.2004.05.002","journal-title":"Ann. Pure Appl. Logic"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-642-15375-4_16","volume-title":"CONCUR 2010 - Concurrency Theory","author":"L Caires","year":"2010","unstructured":"Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 222\u2013236. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_16"},{"key":"9_CR6","unstructured":"Castellan, S., Clairambault, P., Winskel, G.: Observably deterministic concurrent strategies and intensional full abstraction for parallel-or. In: 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, Oxford, UK, 3\u20139 September 2017, pp. 12:1\u201312:16 (2017). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2017.12"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Castellan, S., Yoshida, N.: Causality in linear logic: full completeness and injectivity (unit-free multiplicative-additive fragment). Technical report (2019). http:\/\/iso.mor.phis.me\/publis\/Causality_in_Linear_Logic_FOSSACS19.pdf","DOI":"10.1007\/978-3-030-17127-8_9"},{"key":"9_CR8","unstructured":"Castellan, S., Yoshida, N.: Two sides of the same coin: session types and game semantics. Accepted for publication at POPL 2019 (2019)"},{"key":"9_CR9","series-title":"IFIP International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-0-387-09680-3_26","volume-title":"Fifth Ifip International Conference On Theoretical Computer Science \u2013 Tcs 2008","author":"K Chaudhuri","year":"2008","unstructured":"Chaudhuri, K., Miller, D., Saurin, A.: Canonical sequent proofs via multi-focusing. In: Ausiello, G., Karhum\u00e4ki, J., Mauri, G., Ong, L. (eds.) TCS 2008. IIFIP, vol. 273, pp. 383\u2013396. Springer, Boston, MA (2008). https:\/\/doi.org\/10.1007\/978-0-387-09680-3_26"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/11538363_13","volume-title":"Computer Science Logic","author":"P-L Curien","year":"2005","unstructured":"Curien, P.-L., Faggian, C.: L-nets, strategies and proof-nets. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 167\u2013183. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11538363_13"},{"key":"9_CR11","unstructured":"de Carvalho, D.: The relational model is injective for multiplicative exponential linear logic. In: 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, Marseille, France, 29 August\u20131 September 2016, pp. 41:1\u201341:19 (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2016.41"},{"key":"9_CR12","unstructured":"DeYoung, H., Caires, L., Pfenning, F., Toninho, B.: Cut reduction in linear logic as asynchronous session-typed communication. In: CSL, pp. 228\u2013242 (2012)"},{"key":"9_CR13","unstructured":"Giamberardino, P.D.: Jump from parallel to sequential proofs: additives. Technical report (2011). https:\/\/hal.archives-ouvertes.fr\/hal-00616386"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Faggian, C., Maurel, F.: Ludics nets, a game model of concurrent interaction. In: 20th IEEE Symposium on Logic in Computer Science (LICS 2005), Chicago, IL, USA, 26\u201329 June 2005, Proceedings, pp. 376\u2013385. IEEE Computer Society (2005). http:\/\/dx.doi.org\/10.1109\/LICS.2005.25","DOI":"10.1109\/LICS.2005.25"},{"issue":"4","key":"9_CR15","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.entcs.2007.04.014","volume":"175","author":"C Faggian","year":"2007","unstructured":"Faggian, C., Piccolo, M.: A graph abstract machine describing event structure composition. Electr. Notes Theor. Comput. Sci. 175(4), 21\u201336 (2007). https:\/\/doi.org\/10.1016\/j.entcs.2007.04.014","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/11874683_21","volume-title":"Computer Science Logic","author":"P Di Giamberardino","year":"2006","unstructured":"Di Giamberardino, P., Faggian, C.: Jump from parallel to sequential proofs: multiplicatives. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 319\u2013333. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11874683_21"},{"issue":"1","key":"9_CR17","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. Theor. Comput. Sci. 50(1), 1\u2013101 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Heijltjes, W., Houston, R.: No proof nets for MLL with units: proof equivalence in MLL is PSPACE-complete. In: CSL-LICS 2014, pp. 50:1\u201350:10. ACM (2014)","DOI":"10.1145\/2603088.2603126"},{"issue":"22\u201324","key":"9_CR19","doi-asserted-by":"publisher","first-page":"2223","DOI":"10.1016\/j.tcs.2010.01.028","volume":"411","author":"K Honda","year":"2010","unstructured":"Honda, K., Laurent, O.: An exact correspondence between a typed pi-calculus and polarised proof-nets. Theor. Comput. Sci. 411(22\u201324), 2223\u20132238 (2010). https:\/\/doi.org\/10.1016\/j.tcs.2010.01.028","journal-title":"Theor. Comput. Sci."},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-08918-8_1","volume-title":"Rewriting and Typed Lambda Calculi","author":"K Honda","year":"2014","unstructured":"Honda, K., Yoshida, N., Berger, M.: Process types as a descriptive tool for interaction. In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 1\u201320. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_1"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Hughes, D.J.D., Heijltjes, W.: Conflict nets: efficient locally canonical MALL proof nets. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2016, New York, NY, USA, 5\u20138 July 2016, pp. 437\u2013446 (2016). http:\/\/doi.acm.org\/10.1145\/2933575.2934559","DOI":"10.1145\/2933575.2934559"},{"issue":"4","key":"9_CR22","doi-asserted-by":"publisher","first-page":"784","DOI":"10.1145\/1094622.1094629","volume":"6","author":"DJD Hughes","year":"2005","unstructured":"Hughes, D.J.D., van Glabbeek, R.J.: Proof nets for unit-free multiplicative-additive linear logic. ACM Trans. Comput. Logic 6(4), 784\u2013842 (2005)","journal-title":"ACM Trans. Comput. Logic"},{"issue":"1","key":"9_CR23","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/S0304-3975(01)00297-3","volume":"290","author":"O Laurent","year":"2003","unstructured":"Laurent, O.: Polarized proof-nets and $$\\lambda \\mu $$-calculus. Theor. Comput. Sci. 290(1), 161\u2013188 (2003). https:\/\/doi.org\/10.1016\/S0304-3975(01)00297-3","journal-title":"Theor. Comput. Sci."},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Melli\u00e8s, P.-A.: Asynchronous games 4: a fully complete model of propositional linear logic. In: 20th IEEE Symposium on Logic in Computer Science (LICS 2005), Chicago, IL, USA, 26\u201329 June 2005, Proceedings, pp. 386\u2013395 (2005). http:\/\/dx.doi.org\/10.1109\/LICS.2005.6","DOI":"10.1109\/LICS.2005.6"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/978-3-540-74407-8_27","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"P-A Melli\u00e8s","year":"2007","unstructured":"Melli\u00e8s, P.-A., Mimram, S.: Asynchronous games: innocence without alternation. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 395\u2013411. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_27"},{"key":"9_CR26","unstructured":"Mimram, S.: S\u00e9mantique des jeux asynchrones et r\u00e9\u00e9criture 2-dimensionnelle (asynchronous game semantics and 2-dimensional rewriting systems). Ph.D. thesis, Paris Diderot University, France (2008). https:\/\/tel.archives-ouvertes.fr\/tel-00338643"},{"issue":"2\u20133","key":"9_CR27","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1017\/S095679681400001X","volume":"24","author":"P Wadler","year":"2014","unstructured":"Wadler, P.: Propositions as sessions. J. Funct. Program. 24(2\u20133), 384\u2013418 (2014)","journal-title":"J. Funct. Program."},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/3-540-17906-2_31","volume-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency","author":"G Winskel","year":"1987","unstructured":"Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 255, pp. 325\u2013392. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/3-540-17906-2_31"}],"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-030-17127-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,5]],"date-time":"2025-09-05T18:09:57Z","timestamp":1757095797000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-17127-8_9"}},"subtitle":["Full Completeness and Injectivity (Unit-Free Multiplicative-Additive Fragment)"],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030171261","9783030171278"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17127-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"5 April 2019","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":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}