{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:49Z","timestamp":1775790769409,"version":"3.50.1"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"crossref","award":["EP\/L01503X\/1"],"award-info":[{"award-number":["EP\/L01503X\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Independent Research Fund Denmark","award":["DFF-7014-00041"],"award-info":[{"award-number":["DFF-7014-00041"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>We present Hypersequent Classical Processes (HCP), a revised interpretation of the \u201cProofs as Processes\u201d correspondence between linear logic and the \u03c0-calculus initially proposed by Abramsky [1994], and later developed by Bellin and Scott [1994], Caires and Pfenning [2010], and Wadler [2014], among others. HCP mends the discrepancies between linear logic and the syntax and observable semantics of parallel composition in the \u03c0-calculus, by conservatively extending linear logic to hyperenvironments (collections of environments, inspired by the hypersequents by Avron [1991]). Separation of environments in hyperenvironments is internalised by \u2297 and corresponds to parallel process behaviour. Thanks to this property, for the first time we are able to extract a labelled transition system (lts) semantics from proof rewritings. Leveraging the information on parallelism at the level of types, we obtain a logical reconstruction of the delayed actions that Merro and Sangiorgi [2004] formulated to model non-blocking I\/O in the \u03c0-calculus. We define a denotational semantics for processes based on Brzozowski derivatives, and uncover that non-interference in HCP corresponds to Fubini\u2019s theorem of double antiderivation. Having an lts allows us to validate HCP using the standard toolbox of behavioural theory. We instantiate bisimilarity and barbed congruence for HCP, and obtain a full abstraction result: bisimilarity, denotational equivalence, and barbed congruence coincide.<\/jats:p>","DOI":"10.1145\/3290337","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["Better late than never: a fully-abstract semantics for classical processes"],"prefix":"10.1145","volume":"3","author":[{"given":"Wen","family":"Kokke","sequence":"first","affiliation":[{"name":"University of Edinburgh, UK"}]},{"given":"Fabrizio","family":"Montesi","sequence":"additional","affiliation":[{"name":"University of Southern Denmark, Denmark"}]},{"given":"Marco","family":"Peressotti","sequence":"additional","affiliation":[{"name":"University of Southern Denmark, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00103-0"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_3"},{"key":"e_1_2_2_3_1","volume-title":"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), Sam Lindley, Conor McBride, Philip W","author":"Atkey Robert"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01531058"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001274"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(95)00040-2"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00104-9"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2490818"},{"key":"e_1_2_2_9_1","first-page":"826","article-title":"Behavioural equivalences for coalgebras with unobservable moves","volume":"84","author":"Brengos Tomasz","year":"2015","journal-title":"JLAMP"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/321239.321249"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_9"},{"key":"e_1_2_2_12_1","doi-asserted-by":"crossref","unstructured":"Lu\u00eds Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In CONCUR. 222\u2013236.   Lu\u00eds Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In CONCUR. 222\u2013236.","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_2_2_13_1","first-page":"1","article-title":"Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types","volume":"59","author":"Carbone Marco","year":"2016","journal-title":"CONCUR (LIPIcs)"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-016-0285-y"},{"key":"e_1_2_2_15_1","volume-title":"Gay","author":"Dardha Ornela","year":"2018"},{"key":"e_1_2_2_16_1","volume-title":"26th International Workshop\/21st Annual Conference of the EACSL, CSL 2012","volume":"16","author":"DeYoung Henry","year":"2012"},{"key":"e_1_2_2_17_1","volume-title":"Sugli integrali multipli. Rom. Acc. L. Rend. (5) 16, 1","author":"Fubini G.","year":"1907"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_19_1","doi-asserted-by":"crossref","unstructured":"Kohei Honda Vasco Vasconcelos and Makoto Kubo. 1998. Language primitives and type disciplines for structured communication-based programming. In ESOP. 22\u2013138.   Kohei Honda Vasco Vasconcelos and Makoto Kubo. 1998. Language primitives and type disciplines for structured communication-based programming. In ESOP. 22\u2013138.","DOI":"10.1007\/BFb0053567"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/330249.330251"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-016-0289-7"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951921"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004323"},{"key":"e_1_2_2_25_1","volume-title":"Communication and Concurrency","author":"Milner Robin"},{"key":"e_1_2_2_26_1","volume-title":"Classical Higher-Order Processes. CoRR abs\/1802.02917","author":"Montesi Fabrizio","year":"2018"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.08.001"},{"key":"e_1_2_2_29_1","volume-title":"A structural approach to operational semantics. J. Log. Algebr. Program. 60-61","author":"Plotkin Gordon D.","year":"2004"},{"key":"e_1_2_2_30_1","volume-title":"From pi-Calculus to Higher-Order pi-Calculus - and Back","author":"Sangiorgi Davide"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00075-8"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1889997.1890002"},{"key":"e_1_2_2_33_1","volume-title":"The Pi-Calculus - a theory of mobile processes","author":"Sangiorgi Davide"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_20"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.05.002"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398856.2364568"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.02.011"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290337","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290337","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290337"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":36,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290337"],"URL":"https:\/\/doi.org\/10.1145\/3290337","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}