{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:51Z","timestamp":1780994751087,"version":"3.54.1"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"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":[[2024,10,8]]},"abstract":"<jats:p>Typestate systems are notoriously complex as they require sophisticated machinery for tracking aliasing. We propose a new, transition-oriented foundation for typestate in the setting of impure functional programming. Our approach relies on ordered types for simple alias tracking and its formalization draws on work on bunched implications. Yet, we support a flexible notion of borrowing in the presence of typestate.<\/jats:p>\n                  <jats:p>Our core calculus comes with a notion of resource types indexed by an ordered partial monoid that models abstract state transitions. We prove syntactic type soundness with respect to a resource-instrumented semantics. We give an algorithmic version of our type system and prove its soundness. Algorithmic typing facilitates a simple surface language that does not expose tedious details of ordered types. We implemented a typechecker for the surface language along with an interpreter for the core language.<\/jats:p>","DOI":"10.1145\/3689763","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"1475-1503","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Law and Order for Typestate with Borrowing"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-7014-754X","authenticated-orcid":false,"given":"Hannes","family":"Saffrich","sequence":"first","affiliation":[{"name":"University of Freiburg, Freiburg, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5941-6770","authenticated-orcid":false,"given":"Yuki","family":"Nishida","sequence":"additional","affiliation":[{"name":"Kyoto University, Kyoto, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9000-1239","authenticated-orcid":false,"given":"Peter","family":"Thiemann","sequence":"additional","affiliation":[{"name":"University of Freiburg, Freiburg, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19900360405"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(99)00014-7"},{"issue":"4","key":"e_1_3_1_4_1","first-page":"397","article-title":"L3: A Linear Language with Locations","volume":"77","author":"Ahmed Amal","year":"2007","unstructured":"Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L3: A Linear Language with Locations. Fundam. Informaticae 77, 4 (2007), 397-449. http:\/\/content.iospress.com\/articles\/fundamenta-informaticae\/fi77-4-06","journal-title":"Fundam. Informaticae"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1639950.1640073"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2022.104948"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2022.102844"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297050"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_10"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040329"},{"key":"e_1_3_1_13_1","volume-title":"Aliasing in Object-Oriented Programming. Types, Analysis and Verification . Lecture Notes in Computer Science, Vol. 7850","author":"Clarke Dave","year":"2013","unstructured":"Dave Clarke, James Noble, and Tobias Wrigstad (Eds.). 2013. Aliasing in Object-Oriented Programming. Types, Analysis and Verification . Lecture Notes in Computer Science, Vol. 7850. Springer. https:\/\/doi.org\/10.1007\/978-3-642-36946-9 10.1007\/978-3-642-36946-9"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286947"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3417516"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24851-4_21"},{"key":"e_1_3_1_17_1","unstructured":"Henry DeYoung . 2020. Session-Typed Ordered Logical Specifications. Ph. D. Dissertation.Carnegie Mellon University Pittsburgh PA 15213. https:\/\/www.cs.cmu.edu\/~hdeyoung\/assets\/papers\/thesis20.pdf ."},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_8"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1348250.1348255"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004858"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629609"},{"issue":"4","key":"e_1_3_1_23_1","article-title":"Modular Session Types for Objects","volume":"11","author":"Gay Simon J.","year":"2015","unstructured":"Simon J. Gay, Nils Gesbert, Ant\u00f3nio Ravara, and Vasco Thudichum Vasconcelos. 2015. Modular Session Types for Objects. Log. Methods Comput. Sci. 11,4 (2015). https:\/\/doi.org\/10.2168\/LMCS-11(4:12)2015 10.2168\/LMCS-11(4:12)2015","journal-title":"Log. Methods Comput. Sci"},{"key":"e_1_3_1_24_1","doi-asserted-by":"crossref","unstructured":"Rosita Gerbo and Luca Padovani. 2019. Concurrent Typestate-Oriented Programming in Java. In Proceedings Programming Language Approaches to Concurrency- and Communication-cEntric Software PLACES@ETAPS 2019 Prague Czech Republic 7th April 2019 (EPTCS Vol. 291). 24-34. https:\/\/doi.org\/10.4204\/EPTCS.291.3 10.4204\/EPTCS.291.3","DOI":"10.4204\/EPTCS.291.3"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384619"},{"issue":"1","key":"e_1_3_1_27_1","first-page":"3:1","article-title":"Foundations of Session Types and Behavioural Contracts","volume":"49","author":"H\u00fcttel Hans","year":"2016","unstructured":"Hans H\u00fcttel, Ivan Lanese, Vasco T. Vasconcelos, Lu\u00eds Caires, Marco Carbone, Pierre-Malo Deni\u00e9lou, Dimitris Mostrous, Luca Padovani, Ant\u00f3nio Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. 2016. Foundations of Session Types and Behavioural Contracts. ACM Comput. Surv. 49, 1 (2016), 3:1-3:36. https:\/\/doi.org\/10.1145\/2873052 10.1145\/2873052","journal-title":"ACM Comput. Surv"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503303"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111542.1111550"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(3:4)2006"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1958.11989160"},{"key":"e_1_3_1_32_1","first-page":"166","volume-title":"Structure of Language and Its Mathematical Aspects","author":"Lambek Joachim","year":"1960","unstructured":"Joachim Lambek . 1960. On the Calculus of Syntactic Types. In Structure of Language and Its Mathematical Aspects, Roman Jakobson (Ed.). American Mathematical Society, 166-178. https:\/\/doi.org\/10.1090\/psapm\/012 10.1090\/psapm\/012"},{"key":"e_1_3_1_33_1","article-title":"Functional Ownership through Fractional Uniqueness","author":"Marshall Daniel","year":"2023","unstructured":"Daniel Marshall and Dominic Orchard. 2023. Functional Ownership through Fractional Uniqueness. CoRR abs\/2310.18166 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2310.18166 10.48550\/ARXIV.2310.18166 arXiv:2310.18166","journal-title":"CoRR"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449792"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094818"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268967"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/351268.351277"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/935673"},{"key":"e_1_3_1_42_1","first-page":"295","volume-title":"Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings (Lecture Notes in Computer Science, Vol. 1581)","author":"Polakow Jeff","year":"1999","unstructured":"Jeff Polakow and Frank Pfenning. 1999a. Natural Deduction for Intuitionistic Non-communicative Linear Logic. In Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings (Lecture Notes in Computer Science, Vol. 1581), Jean-Yves Girard (Ed.). Springer, 295-309. https:\/\/doi.org\/10.1007\/3-540-48959-2_21 10.1007\/3-540-48959-2_21"},{"key":"e_1_3_1_43_1","first-page":"449","volume-title":"Fifteenth Conference on Mathematical Foundations of Progamming Semantics, MFPS 1999, Tulane University, New Orleans, LA, USA, April 28 - May 1, 1999 (Electronic Notes in Theoretical Computer Science, Vol. 20)","author":"Polakow Jeff","year":"1999","unstructured":"Jeff Polakow and Frank Pfenning. 1999b. Relating Natural Deduction and Sequent Calculus for Intuitionistic NonCommutative Linear Logic. In Fifteenth Conference on Mathematical Foundations of Progamming Semantics, MFPS 1999, Tulane University, New Orleans, LA, USA, April 28 - May 1, 1999 (Electronic Notes in Theoretical Computer Science, Vol. 20), Stephen D. Brookes, Achim Jung, Michael W. Mislove, and Andre Scedrov (Eds.). Elsevier, 449-466. https:\/\/doi.org\/10.1016\/S1571-0661(04)80088-4 10.1016\/S1571-0661(04)80088-4"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44716-4_4"},{"key":"e_1_3_1_45_1","unstructured":"Hannes Saffrich Yuki Nishida and Peter Thiemann. 2024. Law and Order for Typestate with Borrowing. https:\/\/doi.org\/10.48550\/arXiv.2408.14031 10.48550\/arXiv.2408.14031 arXiv:2408.14031 [cs.PL]"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1924520.1924529"},{"key":"e_1_3_1_47_1","first-page":"11:1","volume-title":"34th International Conference on Concurrency Theory, CONCUR 2023, September 18-23, 2023, Antwerp, Belgium (LIPIcs, Vol. 279)","author":"Silva Gil","year":"2023","unstructured":"Gil Silva, Andreia Mordido, and Vasco T. Vasconcelos. 2023. Subtyping Context-Free Session Types. In 34th International Conference on Concurrency Theory, CONCUR 2023, September 18-23, 2023, Antwerp, Belgium (LIPIcs, Vol. 279), Guillermo A. P\u00e9rez and Jean-Fran\u00e7ois Raskin (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 11:1-11:19.https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2023.11 10.4230\/LIPICS.CONCUR.2023.11"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547626"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.232013"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312929"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.2197\/ipsjtrans.1.53"},{"key":"e_1_3_1_52_1","unstructured":"The Rust Team. 2024. The Rust Programming Language. http:\/\/rust-lang.org\/."},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926436"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-50086-3_12"},{"key":"e_1_3_1_55_1","first-page":"561","volume-title":"Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler . 1990. Linear Types can Change the World!. In Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 2-5 April, 1990. North-Holland, 561."},{"key":"e_1_3_1_56_1","volume-title":"Advanced Topics in Types and Programming Languages","author":"Walker David","year":"2005","unstructured":"David Walker . 2005. Substructural Type Systems. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). MIT Press, Chapter 1. https:\/\/doi.org\/10.7551\/mitpress\/1104.003.0003 10.7551\/mitpress\/1104.003.0003"},{"key":"e_1_3_1_57_1","doi-asserted-by":"crossref","unstructured":"Max Willsey Rokhini Prabhu and Frank Pfenning. 2016. Design and Implementation of Concurrent C0. In Proceedings Fourth International Workshop on Linearity LINEARITY 2016 Porto Portugal 25 June 2016 (EPTCS Vol. 238). 73-82. https:\/\/doi.org\/10.4204\/EPTCS.238.8 10.4204\/EPTCS.238.8","DOI":"10.4204\/EPTCS.238.8"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689763","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689763","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:04:07Z","timestamp":1770195847000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689763"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":56,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689763"],"URL":"https:\/\/doi.org\/10.1145\/3689763","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-05","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}