{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:24:45Z","timestamp":1750307085303,"version":"3.41.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,1,23]],"date-time":"2013-01-23T00:00:00Z","timestamp":1358899200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGPLAN Not."],"published-print":{"date-parts":[[2013,1,23]]},"abstract":"<jats:p>We introduce the concept of behavioral separation as a general principle for disciplining interference in higher-order imperative concurrent programs, and present a type-based approach that systematically develops the concept in the context of an ML-like language extended with concurrency and synchronization primitives. Behavioral separation builds on notions originally introduced for behavioral type systems and separation logics, but shifts the focus from the separation of static program state properties towards the separation of dynamic usage behaviors of runtime values. Behavioral separation types specify how values may be safely used by client code, and can enforce fine-grained interference control disciplines while preserving compositionality, information hiding, and flexibility. We illustrate how our type system, even if based on a small set of general primitives, is already able to tackle fairly challenging program idioms, involving aliasing at various types, concurrency with first-class threads, manipulation of linked data structures, behavioral borrowing, and invariant-based separation.<\/jats:p>","DOI":"10.1145\/2480359.2429103","type":"journal-article","created":{"date-parts":[[2016,11,9]],"date-time":"2016-11-09T20:38:28Z","timestamp":1478723908000},"page":"275-286","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["The type discipline of behavioral separation"],"prefix":"10.1145","volume":"48","author":[{"given":"Lu\u00eds","family":"Caires","sequence":"first","affiliation":[{"name":"Universidade Nova de Lisboa, Lisboa, Portugal"}]},{"given":"Jo\u00e3o C.","family":"Seco","sequence":"additional","affiliation":[{"name":"Universidade Nova de Lisboa, Lisboa, Portugal"}]}],"member":"320","published-online":{"date-parts":[[2013,1,23]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1119479.1119480"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1365997.1366003"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297050"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00230-8"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/582419.582440"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604156"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/504282.504287"},{"key":"e_1_2_2_9_1","first-page":"55","volume-title":"Checking Interference with Fractional Permissions. In SAS 2003","volume":"2694","author":"Boyland J.","year":"2003","unstructured":"J. Boyland . Checking Interference with Fractional Permissions. In SAS 2003 , volume 2694 of LNCS, pages 55 -- 72 . Springer-Verlag , 2003 . J. Boyland. Checking Interference with Fractional Permissions. In SAS 2003, volume 2694 of LNCS, pages 55--72. Springer-Verlag, 2003."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.04.030"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00137-8"},{"key":"e_1_2_2_12_1","series-title":"LNCS","first-page":"222","volume-title":"CONCUR'10","author":"Caires L.","year":"2010","unstructured":"L. Caires and F. Pfenning . Session Types as Intuitionistic Linear Propositions . In CONCUR'10 , volume 6269 of LNCS , pages 222 -- 236 . Springer-Verlag , 2010 . L. Caires and F. Pfenning. Session Types as Intuitionistic Linear Propositions. In CONCUR'10, volume 6269 of LNCS, pages 222--236. Springer-Verlag, 2010."},{"key":"e_1_2_2_13_1","volume-title":"TR-DI-FCT-UNL","author":"Caires L.","year":"2012","unstructured":"L. Caires and J. C. Seco . The Type Discipline of Behavioral Separation. Technical report , TR-DI-FCT-UNL , 2012 . L. Caires and J. C. Seco. The Type Discipline of Behavioral Separation. Technical report, TR-DI-FCT-UNL, 2012."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325742"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503278"},{"key":"e_1_2_2_17_1","first-page":"504","volume-title":"Concurrent Abstract Predicates. In ECOOP 2010","volume":"6183","author":"Dinsdale-Young T.","year":"2010","unstructured":"T. Dinsdale-Young , M. Dodds , P. Gardner , M. J. Parkinson , and V. Vafeiadis . Concurrent Abstract Predicates. In ECOOP 2010 , volume 6183 of LNCS, pages 504 -- 528 . Springer-Verlag , 2010 . T. Dinsdale-Young, M. Dodds, P. Gardner, M. J. Parkinson, and V. Vafeiadis. Concurrent Abstract Predicates. In ECOOP 2010, volume 6183 of LNCS, pages 504--528. Springer-Verlag, 2010."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706335"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_27"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.04.050"},{"key":"e_1_2_2_21_1","first-page":"122","volume-title":"Language Primitives and Type Discipline for Structured Communication-Based Programming. In ESOP 1998","volume":"1381","author":"Honda K.","year":"1998","unstructured":"K. Honda , V. T. Vasconcelos , and M. Kubo . Language Primitives and Type Discipline for Structured Communication-Based Programming. In ESOP 1998 , volume 1381 of LNCS, pages 122 -- 138 . Springer , 1998 . K. Honda, V. T. Vasconcelos, and M. Kubo. Language Primitives and Type Discipline for Structured Communication-Based Programming. In ESOP 1998, volume 1381 of LNCS, pages 122--138. Springer, 1998."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503303"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00325-6"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.029"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926447"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364536"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1924520.1924527"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103722"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004495"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_2_34_1","volume-title":"Types and Programming Languages","author":"Pierce B.","year":"2002","unstructured":"B. Pierce . Types and Programming Languages . MIT Press , 2002 . B. Pierce. Types and Programming Languages. MIT Press, 2002."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.16"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512766"},{"key":"e_1_2_2_37_1","series-title":"LNCS","first-page":"704","volume-title":"ICALP 89","author":"Reynolds J. C.","year":"1989","unstructured":"J. C. Reynolds . Syntactic Control of Interference, Part 2 . In ICALP 89 , volume 372 of LNCS , pages 704 -- 722 . Springer , 1989 . J. C. Reynolds. Syntactic Control of Interference, Part 2. In ICALP 89, volume 372 of LNCS, pages 704--722. Springer, 1989."},{"key":"e_1_2_2_38_1","first-page":"173","volume-title":"Design of the programming language FORSYTHE","author":"Reynolds J. C.","year":"1997","unstructured":"J. C. Reynolds . Design of the programming language FORSYTHE , pages 173 -- 233 . Birkhauser Boston Inc ., Cambridge, MA, USA, 1997 . J. C. Reynolds. Design of the programming language FORSYTHE, pages 173--233. Birkhauser Boston Inc., Cambridge, MA, USA, 1997."},{"key":"e_1_2_2_39_1","volume-title":"Separation Logic: A Logic for Shared Mutable Data Structures. In LICS 2012","author":"Reynolds J. C.","year":"2002","unstructured":"J. C. Reynolds . Separation Logic: A Logic for Shared Mutable Data Structures. In LICS 2012 , 2002 . J. C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS 2012, 2002."},{"key":"e_1_2_2_40_1","volume-title":"Nested Hoare Triples and Frame Rules for Higher-order Store. Logical Methods in Computer Science, 7(3)","author":"Schwinghammer J.","year":"2011","unstructured":"J. Schwinghammer , L. Birkedal , B. Reus , and H. Yang . Nested Hoare Triples and Frame Rules for Higher-order Store. Logical Methods in Computer Science, 7(3) , 2011 . J. Schwinghammer, L. Birkedal, B. Reus, and H. Yang. Nested Hoare Triples and Frame Rules for Higher-order Store. Logical Methods in Computer Science, 7(3), 2011."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_15"}],"container-title":["ACM SIGPLAN Notices"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2480359.2429103","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2480359.2429103","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:34:20Z","timestamp":1750239260000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2480359.2429103"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1,23]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,1,23]]}},"alternative-id":["10.1145\/2480359.2429103"],"URL":"https:\/\/doi.org\/10.1145\/2480359.2429103","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2429069.2429103","asserted-by":"subject"}]},"ISSN":["0362-1340","1558-1160"],"issn-type":[{"type":"print","value":"0362-1340"},{"type":"electronic","value":"1558-1160"}],"subject":[],"published":{"date-parts":[[2013,1,23]]},"assertion":[{"value":"2013-01-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}