{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:12:46Z","timestamp":1775873566041,"version":"3.50.1"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2014,10,28]],"date-time":"2014-10-28T00:00:00Z","timestamp":1414454400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["#0937060"],"award-info":[{"award-number":["#0937060"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100005651","name":"Computing Research Association","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100005651","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002850","name":"Fondo Nacional de Desarrollo Cient\u00edfico y Tecnol\u00f3gico","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002850","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["#CCF-0811592 and #CCF-1116907"],"award-info":[{"award-number":["#CCF-0811592 and #CCF-1116907"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2014,10,28]]},"abstract":"<jats:p>Typestate reflects how the legal operations on imperative objects can change at runtime as their internal state changes. A typestate checker can statically ensure, for instance, that an object method is only called when the object is in a state for which the operation is well defined. Prior work has shown how modular typestate checking can be achieved thanks to access permissions and state guarantees. However, typestate was not treated as a primitive language concept: typestate checkers are an additional verification layer on top of an existing language. In contrast, a typestate-oriented programming (TSOP) language directly supports expressing typestates. For example, in the Plaid programming language, the typestate of an object directly corresponds to its class, and that class can change dynamically. Plaid objects have not only typestate-dependent interfaces but also typestate-dependent behaviors and runtime representations.<\/jats:p>\n          <jats:p>This article lays foundations for TSOP by formalizing a nominal object-oriented language with mutable state that integrates typestate change and typestate checking as primitive concepts. We first describe a statically typed language\u2014Featherweight Typestate (FT)\u2014where the types of object references are augmented with access permissions and state guarantees. We describe a novel flow-sensitive permission-based type system for FT. Because static typestate checking is still too rigid for some applications, we then extend this language into a gradually typed language\u2014Gradual Featherweight Typestate (GFT). This language extends the notion of gradual typing to account for typestate: gradual typestate checking seamlessly combines static and dynamic checking by automatically inserting runtime checks into programs. The gradual type system of GFT allows programmers to write dynamically safe code even when the static type checker can only partly verify it.<\/jats:p>","DOI":"10.1145\/2629609","type":"journal-article","created":{"date-parts":[[2014,10,29]],"date-time":"2014-10-29T18:05:55Z","timestamp":1414605955000},"page":"1-44","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":65,"title":["Foundations of Typestate-Oriented Programming"],"prefix":"10.1145","volume":"36","author":[{"given":"Ronald","family":"Garcia","sequence":"first","affiliation":[{"name":"University of British Columbia"}]},{"given":"\u00c9ric","family":"Tanter","sequence":"additional","affiliation":[{"name":"University of Chile"}]},{"given":"Roger","family":"Wolff","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University"}]},{"given":"Jonathan","family":"Aldrich","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University"}]}],"member":"320","published-online":{"date-parts":[[2014,10,28]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1365997.1366003"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1639950.1640073"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/185009.185016"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297050"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_10"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1883978.1883986"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806805"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1760267.1760273"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040329"},{"key":"e_1_2_1_10_1","series-title":"Lecture Notes in Computer Science","volume-title":"ECOOP 2004\u2014Object-Oriented Programming","author":"DeLine Robert","unstructured":"Robert DeLine and Manuel F\u00e4hndrich. 2004. Typestates for objects. In ECOOP 2004\u2014Object-Oriented Programming. Lecture Notes in Computer Science, Vol. 3086. Springer, 465--490."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/646158.680007"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1348250.1348255"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/186897"},{"key":"e_1_2_1_14_1","volume-title":"Technical Report CMU-ISR-13-112","author":"Garcia Ronald","unstructured":"Ronald Garcia, Roger Wolff, \u00c9ric Tanter, and Jonathan Aldrich. 2013. Featherweight Typestate. Technical Report CMU-ISR-13-112. Carnegie Mellon University, Pittsburgh, PA."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706335"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503505"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_3"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111596.1111597"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103722"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449792"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094818"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019462"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1924520.1924529"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the Scheme and Functional Programming Workshop. ACM","author":"Siek Jeremy","year":"2006","unstructured":"Jeremy Siek and Walid Taha. 2006. Gradual typing for functional languages. In Proceedings of the Scheme and Functional Programming Workshop. ACM, New York, NY."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/2394758.2394762"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1408681.1408688"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312929"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048122"},{"key":"e_1_2_1_33_1","volume-title":"Advanced Topics in Types and Programming Languages","author":"Walker David","unstructured":"David Walker. 2005. Substructural type systems. In Advanced Topics in Types and Programming Languages, Benjamin Pierce (Ed.). MIT Press, Cambridge, MA, 3--43."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032497.2032529"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629609","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2629609","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:13:29Z","timestamp":1750227209000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629609"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10,28]]},"references-count":33,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,10,28]]}},"alternative-id":["10.1145\/2629609"],"URL":"https:\/\/doi.org\/10.1145\/2629609","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,10,28]]},"assertion":[{"value":"2012-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-10-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}