{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:11Z","timestamp":1751660531728,"version":"3.41.0"},"reference-count":63,"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\/"}],"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 develop a principled integration of shared mutable state into a proposition-as-types linear logic interpretation of a session-based concurrent programming language. While the foundation of type systems for the functional core of programming languages often builds on the proposition-as-types correspondence, automatically ensuring strong safety and liveness properties, imperative features have mostly been handled by extra-logical constructions. Our system crucially builds on the integration of nondeterminism and sharing, inspired by logical rules of differential linear logic, and ensures session fidelity, progress, confluence and normalisation, while being able to handle first-class shareable reference cells storing any persistent object. We also show how preservation and, perhaps surprisingly, progress, resiliently survive in a natural extension of our language with first-class locks. We illustrate the expressiveness of our language with examples highlighting detailed features, up to simple shareable concurrent ADTs.<\/jats:p>","DOI":"10.1145\/3473584","type":"journal-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T10:44:29Z","timestamp":1629369869000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Propositions-as-types and shared state"],"prefix":"10.1145","volume":"5","author":[{"given":"Pedro","family":"Rocha","sequence":"first","affiliation":[{"name":"Nova University of Lisbon, Portugal"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3215-6734","authenticated-orcid":false,"given":"Lu\u00eds","family":"Caires","sequence":"additional","affiliation":[{"name":"Nova University of Lisbon, Portugal"}]}],"member":"320","published-online":{"date-parts":[[2021,8,19]]},"reference":[{"key":"e_1_2_2_1_1","first-page":"397","article-title":"L^3","volume":"77","author":"Ahmed Amal","year":"2007","unstructured":"Amal Ahmed , Matthew Fluet , and Greg Morrisett . 2007 . L^3 : A Linear Language with Locations. Fundam. Inf. , 77 , 4 (2007), Dec. , 397 \u2013 449 . issn:0169-2968 Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L^3: A Linear Language with Locations. Fundam. Inf., 77, 4 (2007), Dec., 397\u2013449. issn:0169-2968","journal-title":"A Linear Language with Locations. Fundam. Inf."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_2"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110281"},{"volume-title":"Manifest Deadlock-Freedom for Shared Session Types","author":"Balzer Stephanie","key":"e_1_2_2_5_1","unstructured":"Stephanie Balzer , Bernardo Toninho , and Frank Pfenning . 2019. Manifest Deadlock-Freedom for Shared Session Types . In Programming Languages and Systems, Lu\u00eds Caires (Ed.). Springer International Publishing , Cham . 611\u2013639. isbn:978-3-030-17184-1 Stephanie Balzer, Bernardo Toninho, and Frank Pfenning. 2019. Manifest Deadlock-Freedom for Shared Session Types. In Programming Languages and Systems, Lu\u00eds Caires (Ed.). Springer International Publishing, Cham. 611\u2013639. isbn:978-3-030-17184-1"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.40"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61604-7_54"},{"key":"e_1_2_2_8_1","volume-title":"P\u00e9rez","author":"Caires Lu\u00eds","year":"2016","unstructured":"Lu\u00eds Caires and Jorge A . P\u00e9rez . 2016 . Multiparty Session Types Within a Canonical Binary Theory, and Beyond. In Formal Techniques for Distributed Objects, Components, and Systems, Elvira Albert and Ivan Lanese (Eds.). Springer International Publishing , Cham. 74\u201395. isbn:978-3-319-39570-8 Lu\u00eds Caires and Jorge A. P\u00e9rez. 2016. Multiparty Session Types Within a Canonical Binary Theory, and Beyond. In Formal Techniques for Distributed Objects, Components, and Systems, Elvira Albert and Ivan Lanese (Eds.). Springer International Publishing, Cham. 74\u201395. isbn:978-3-319-39570-8"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_9"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_19"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103786.2103788"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000218"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429103"},{"key":"e_1_2_2_15_1","volume-title":"27 International Conference on Concurrency Theory (CONCUR\u201916)","author":"Carbone Marco","year":"2016","unstructured":"Marco Carbone , Sam Lindley , Fabrizio Montesi , Carsten Sch\u00fcrmann , and Philip Wadler . 2016 . Coherence Generalises Duality: a logical explanation of multiparty session types . In 27 International Conference on Concurrency Theory (CONCUR\u201916) . Qu\u00e9bec City, Canada. https:\/\/hal.inria.fr\/hal-01336600 Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Sch\u00fcrmann, and Philip Wadler. 2016. Coherence Generalises Duality: a logical explanation of multiparty session types. In 27 International Conference on Concurrency Theory (CONCUR\u201916). Qu\u00e9bec City, Canada. https:\/\/hal.inria.fr\/hal-01336600"},{"key":"e_1_2_2_16_1","unstructured":"Luca Cardelli. 1991. Typeful Programming. IFIP State-of-the-Art Reports: Formal Description of Programming Concepts 431\u2013507.  Luca Cardelli. 1991. Typeful Programming. IFIP State-of-the-Art Reports: Formal Description of Programming Concepts 431\u2013507."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286947"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378811"},{"key":"e_1_2_2_20_1","volume-title":"Ugo de\u2019Liguoro, and Nobuko Yoshida","author":"Dezani-Ciancaglini Mariangiola","year":"2008","unstructured":"Mariangiola Dezani-Ciancaglini , Ugo de\u2019Liguoro, and Nobuko Yoshida . 2008 . On Progress for Structured Communications. In Trustworthy Global Computing, Gilles Barthe and C\u00e9dric Fournet (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg. 257\u2013275. isbn:978-3-540-78663-4 Mariangiola Dezani-Ciancaglini, Ugo de\u2019Liguoro, and Nobuko Yoshida. 2008. On Progress for Structured Communications. In Trustworthy Global Computing, Gilles Barthe and C\u00e9dric Fournet (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 257\u2013275. isbn:978-3-540-78663-4"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000372"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.06.005"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00392-X"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.003"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90069-8"},{"key":"e_1_2_2_27_1","unstructured":"Jean-Yves Girard Paul Taylor and Yves Lafont. 1989. Proofs and Types. Cambridge University Press USA. isbn:0521371813  Jean-Yves Girard Paul Taylor and Yves Lafont. 1989. Proofs and Types. Cambridge University Press USA. isbn:0521371813"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"e_1_2_2_29_1","volume-title":"Logic programming in a fragment of intuitionistic linear logic. Information and computation, 110, 2","author":"Hodas Joshua S","year":"1994","unstructured":"Joshua S Hodas and Dale Miller . 1994. Logic programming in a fragment of intuitionistic linear logic. Information and computation, 110, 2 ( 1994 ), 327\u2013365. Joshua S Hodas and Dale Miller. 1994. Logic programming in a fragment of intuitionistic linear logic. Information and computation, 110, 2 (1994), 327\u2013365."},{"volume-title":"CONCUR\u201993","author":"Honda Kohei","key":"e_1_2_2_30_1","unstructured":"Kohei Honda . 1993. Types for dyadic interaction . In CONCUR\u201993 , Eike Best (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 509\u2013523. isbn:978-3-540-47968-0 Kohei Honda. 1993. Types for dyadic interaction. In CONCUR\u201993, Eike Best (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 509\u2013523. isbn:978-3-540-47968-0"},{"volume-title":"Language primitives and type discipline for structured communication-based programming","author":"Honda Kohei","key":"e_1_2_2_31_1","unstructured":"Kohei Honda , Vasco T. Vasconcelos , and Makoto Kubo . 1998. Language primitives and type discipline for structured communication-based programming . In Programming Languages and Systems, Chris Hankin (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 122\u2013138. isbn:978-3-540-69722-0 Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. 1998. Language primitives and type discipline for structured communication-based programming. In Programming Languages and Systems, Chris Hankin (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 122\u2013138. isbn:978-3-540-69722-0"},{"volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Howard W. A.","key":"e_1_2_2_32_1","unstructured":"W. A. Howard . 1980. The formulae-as-types notion of construction . In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism , J. P. Seldin and J. R. Hindley (Eds.). Academic Press , 479\u2013490. W. A. Howard. 1980. The formulae-as-types notion of construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. P. Seldin and J. R. Hindley (Eds.). Academic Press, 479\u2013490."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"volume-title":"Towards Races in Linear Logic","author":"Kokke Wen","key":"e_1_2_2_35_1","unstructured":"Wen Kokke , J. Garrett Morris , and Philip Wadler . 2019. Towards Races in Linear Logic . In Coordination Models and Languages, Hanne Riis Nielson and Emilio Tuosto (Eds.). Springer International Publishing , Cham . 37\u201353. isbn:978-3-030-22397-7 Wen Kokke, J. Garrett Morris, and Philip Wadler. 2019. Towards Races in Linear Logic. In Coordination Models and Languages, Hanne Riis Nielson and Emilio Tuosto (Eds.). Springer International Publishing, Cham. 37\u201353. isbn:978-3-030-22397-7"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364536"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/800141.804654"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2016.16"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/44501.45065"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/331605.331611"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511530104"},{"volume-title":"Programming Languages and Systems","author":"Pagani Michele","key":"e_1_2_2_44_1","unstructured":"Michele Pagani and Paolo Tranquilli . 2009. Parallel Reduction in Resource Lambda-Calculus . In Programming Languages and Systems , Zhenjiang Hu (Ed.). Springer Berlin Heidelberg, Berlin , Heidelberg . 226\u2013242. isbn:978-3-642-10672-9 Michele Pagani and Paolo Tranquilli. 2009. Parallel Reduction in Resource Lambda-Calculus. In Programming Languages and Systems, Zhenjiang Hu (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 226\u2013242. isbn:978-3-642-10672-9"},{"volume-title":"Linear Logical Relations for Session-Based Concurrency","author":"P\u00e9rez Jorge A.","key":"e_1_2_2_45_1","unstructured":"Jorge A. P\u00e9rez , Lu\u00eds Caires , Frank Pfenning , and Bernardo Toninho . 2012. Linear Logical Relations for Session-Based Concurrency . In Programming Languages and Systems, Helmut Seidl (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 539\u2013558. isbn:978-3-642-28869-2 Jorge A. P\u00e9rez, Lu\u00eds Caires, Frank Pfenning, and Bernardo Toninho. 2012. Linear Logical Relations for Session-Based Concurrency. In Programming Languages and Systems, Helmut Seidl (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 539\u2013558. isbn:978-3-642-28869-2"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158524"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/788017.788741"},{"volume-title":"Foundations of Software Science and Computation Structures","author":"Pfenning Frank","key":"e_1_2_2_48_1","unstructured":"Frank Pfenning and Dennis Griffith . 2015. Polarized Substructural Session Types . In Foundations of Software Science and Computation Structures , Andrew Pitts (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 3\u201322. isbn:978-3-662-46678-0 Frank Pfenning and Dennis Griffith. 2015. Polarized Substructural Session Types. In Foundations of Software Science and Computation Structures, Andrew Pitts (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 3\u201322. isbn:978-3-662-46678-0"},{"key":"e_1_2_2_49_1","volume-title":"Types and Programming Languages","author":"Pierce Benjamin C.","year":"2091","unstructured":"Benjamin C. Pierce . 2002. Types and Programming Languages ( 1 st ed.). The MIT Press . isbn:026216 2091 Benjamin C. Pierce. 2002. Types and Programming Languages (1st ed.). The MIT Press. isbn:0262162091","edition":"1"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205035"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473567"},{"key":"e_1_2_2_52_1","unstructured":"Pedro Rocha and Lu\u00eds Caires. 2021. A Propositions-as-Types System for Shared State. NOVA Laboratory for Computer Science and Informatics. http:\/\/ctp.di.fct.unl.pt\/~lcaires\/papers\/PTSStech-report2021.pdf  Pedro Rocha and Lu\u00eds Caires. 2021. A Propositions-as-Types System for Shared State. NOVA Laboratory for Computer Science and Informatics. http:\/\/ctp.di.fct.unl.pt\/~lcaires\/papers\/PTSStech-report2021.pdf"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5037493"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00040-7"},{"volume-title":"PI-Calculus: A Theory of Mobile Processes","author":"Sangiorgi Davide","key":"e_1_2_2_55_1","unstructured":"Davide Sangiorgi and David Walker . 2001. PI-Calculus: A Theory of Mobile Processes . Cambridge University Press , USA. isbn:0521781779 Davide Sangiorgi and David Walker. 2001. PI-Calculus: A Theory of Mobile Processes. Cambridge University Press, USA. isbn:0521781779"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048122"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2003476.2003499"},{"volume-title":"Higher-Order Processes, Functions, and Sessions: A Monadic Integration","author":"Toninho Bernardo","key":"e_1_2_2_58_1","unstructured":"Bernardo Toninho , Luis Caires , and Frank Pfenning . 2013. Higher-Order Processes, Functions, and Sessions: A Monadic Integration . In Programming Languages and Systems, Matthias Felleisen and Philippa Gardner (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 350\u2013369. isbn:978-3-642-37036-6 Bernardo Toninho, Luis Caires, and Frank Pfenning. 2013. Higher-Order Processes, Functions, and Sessions: A Monadic Integration. In Programming Languages and Systems, Matthias Felleisen and Philippa Gardner (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 350\u2013369. isbn:978-3-642-37036-6"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3457884"},{"issue":"2","key":"e_1_2_2_60_1","first-page":"2","article-title":"Linear Types can Change the World!","volume":"2","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler . 1990 . Linear Types can Change the World! . In Proceedings of the IFIP Working Group 2 . 2 , 2 .3 Working Conference on Programming Concepts and Methods, 1990, Manfred Broy (Ed.). North-Holland, 561. Philip Wadler. 1990. Linear Types can Change the World!. In Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, 1990, Manfred Broy (Ed.). North-Holland, 561.","journal-title":"Proceedings of the IFIP Working Group"},{"key":"e_1_2_2_61_1","unstructured":"Philip Wadler. 1990. Recursive types for free.  Philip Wadler. 1990. Recursive types for free."},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364568"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699407"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473584","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473584","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:16Z","timestamp":1750195696000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473584"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,19]]},"references-count":63,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2021,8,22]]}},"alternative-id":["10.1145\/3473584"],"URL":"https:\/\/doi.org\/10.1145\/3473584","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"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"}}]}}