{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,16]],"date-time":"2026-05-16T06:49:57Z","timestamp":1778914197552,"version":"3.51.4"},"reference-count":75,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T00:00:00Z","timestamp":1629331200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["12386,25804"],"award-info":[{"award-number":["12386,25804"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,8,22]]},"abstract":"<jats:p>We introduce coexponentials, a new set of modalities for Classical Linear Logic. As duals to exponentials, the coexponentials codify a distributed form of the structural rules of weakening and contraction. This makes them a suitable logical device for encapsulating the pattern of a server receiving requests from an arbitrary number of clients on a single channel. Guided by this intuition we formulate a system of session types based on Classical Linear Logic with coexponentials, which is suited to modelling client-server interactions. We also present a session-typed functional programming language for client-server programming, which we translate to our system of coexponentials.<\/jats:p>","DOI":"10.1145\/3473567","type":"journal-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T10:44:29Z","timestamp":1629369869000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Client-server sessions in linear logic"],"prefix":"10.1145","volume":"5","author":[{"given":"Zesen","family":"Qian","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G. A.","family":"Kavvos","sequence":"additional","affiliation":[{"name":"University of Bristol, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,8,19]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90181-R"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3503-6_5"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00103-0"},{"key":"e_1_2_2_4_1","volume-title":"Subseries F)","author":"Abramsky Samson"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275407"},{"key":"e_1_2_2_6_1","volume-title":"Parallel Computing: Theory and Practice","author":"Acar Umut A","year":"2016"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371086"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_3"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_2"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01531058"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2071368.2071370"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110281"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_22"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001274"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002326"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00104-9"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561458"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/209936.209958"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_9"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1887654.1887670"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000218"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2016.33"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-016-0285-y"},{"key":"e_1_2_2_24_1","volume-title":"Game Semantics: Easy as Pi. CoRR, abs\/2011.05248","author":"Castellan Simon","year":"2020"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1463822.1463838"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000188"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/99.660313"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_5"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.190.1"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00004"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926435"},{"key":"e_1_2_2_32_1","unstructured":"Farzaneh Derakhshan and Frank Pfenning. 2020. Circular Proofs in First-Order Linear Logic with Least and Greatest Fixed Points. arxiv:2001.05132.  Farzaneh Derakhshan and Frank Pfenning. 2020. Circular Proofs in First-Order Linear Logic with Least and Greatest Fixed Points. arxiv:2001.05132."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000372"},{"key":"e_1_2_2_34_1","volume-title":"Categorical models of Linear Logic with fixed points of formulas. arxiv:2011.10209. To appear in the proceedings of LICS","author":"Ehrhard Thomas","year":"2021"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.06.005"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290341"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014972"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/800055.802017"},{"key":"e_1_2_2_42_1","volume-title":"The Art of Multiprocessor Programming (revised","author":"Herlihy Maurice"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_2_2_46_1","volume-title":"The General Theory of Employment, Interest and Money","author":"Keynes John Maynard"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2002.3171"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40007-3_26"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_16"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.292.5"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290337"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-22397-7_3"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151629"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1639949.1640106"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_23"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951921"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.13052\/rp-9788793519817"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00358-2"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00022-2"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000402"},{"key":"e_1_2_2_61_1","unstructured":"Paul-Andr\u00e9 Melli\u00e8s. 2009. Categorical Semantics of Linear Logic. In Panoramas et synth\u00e8ses 27: Interactive models of computation and program behaviour Pierre-Louis Curien Hugo Herbelin Jean-Louis Krivine and Paul-Andr\u00e9 Melli\u00e8s (Eds.). Soci\u00e9t\u00e9 Math\u00e9matique de France. isbn:978-2-85629-273-0 http:\/\/www.pps.univ-paris-diderot.fr\/~mellies\/papers\/panorama.pdf  Paul-Andr\u00e9 Melli\u00e8s. 2009. Categorical Semantics of Linear Logic. In Panoramas et synth\u00e8ses 27: Interactive models of computation and program behaviour Pierre-Louis Curien Hugo Herbelin Jean-Louis Krivine and Paul-Andr\u00e9 Melli\u00e8s (Eds.). Soci\u00e9t\u00e9 Math\u00e9matique de France. isbn:978-2-85629-273-0 http:\/\/www.pps.univ-paris-diderot.fr\/~mellies\/papers\/panorama.pdf"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000426"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004323"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001407"},{"key":"e_1_2_2_65_1","volume-title":"Communicating and Mobile Systems: The \u03c0 -calculus","author":"Milner Robin"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_2_67_1","unstructured":"Fabrizio Montesi and Marco Peressotti. 2018. Classical Transitions. arxiv:1803.01049.  Fabrizio Montesi and Marco Peressotti. 2018. Classical Transitions. arxiv:1803.01049."},{"key":"e_1_2_2_68_1","unstructured":"Jason Reed. 2009. A Judgmental Deconstruction of Modal Logic. http:\/\/www.cs.cmu.edu\/~jcreed\/papers\/jdml.pdf  Jason Reed. 2009. A Judgmental Deconstruction of Modal Logic. http:\/\/www.cs.cmu.edu\/~jcreed\/papers\/jdml.pdf"},{"key":"e_1_2_2_69_1","volume-title":"Intel threading building blocks: outfitting C++ for multi-core processor parallelism. \" O\u2019Reilly Media","author":"Reinders James"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473584"},{"key":"e_1_2_2_71_1","volume-title":"Manifestly Phased Communication via Shared Session Types. CoRR, abs\/2101.06249","author":"Sano Chuta","year":"2021"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-45917-1_11"},{"key":"e_1_2_2_73_1","volume-title":"Tanenbaum","author":"van Steen Maarten","year":"2017"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.05.002"},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681400001X"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473567","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473567","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:15Z","timestamp":1750195695000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473567"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,19]]},"references-count":75,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2021,8,22]]}},"alternative-id":["10.1145\/3473567"],"URL":"https:\/\/doi.org\/10.1145\/3473567","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,19]]},"assertion":[{"value":"2021-08-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}