{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:08:28Z","timestamp":1774987708208,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,6,16]],"date-time":"2013-06-16T00:00:00Z","timestamp":1371340800000},"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":[],"published-print":{"date-parts":[[2013,6,16]]},"DOI":"10.1145\/2491956.2462160","type":"proceedings-article","created":{"date-parts":[[2013,6,11]],"date-time":"2013-06-11T12:03:50Z","timestamp":1370952230000},"page":"73-84","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Rely-guarantee references for refinement types over aliased mutable data"],"prefix":"10.1145","author":[{"given":"Colin S.","family":"Gordon","sequence":"first","affiliation":[{"name":"University of Washington, Seattle, WA, USA"}]},{"given":"Michael D.","family":"Ernst","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, WA, USA"}]},{"given":"Dan","family":"Grossman","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, WA, USA"}]}],"member":"320","published-online":{"date-parts":[[2013,6,16]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289451"},{"key":"e_1_3_2_1_2_1","volume-title":"Lambda Calculi with Types","author":"Barendregt H.","year":"1991","unstructured":"H. Barendregt . Lambda Calculi with Types . 1991 . H. Barendregt. Lambda Calculi with Types. 1991."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1953122.1953145"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Bertot Y.","year":"2004","unstructured":"Y. Bertot and P. Cast\u00e9ran . Interactive Theorem Proving and Program Development ; Coq'Art: The Calculus of Inductive Constructions. Springer Verlag , 2004 . Y. Bertot and P. Cast\u00e9ran. Interactive Theorem Proving and Program Development; Coq'Art: The Calculus of Inductive Constructions. Springer Verlag, 2004."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297050"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640097"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_3_2_1_8_1","volume-title":"March","author":"Capretta V.","year":"2004","unstructured":"V. Capretta . A Polymorphic Representation of Induction-Recursion. Retrieved 9\/12\/12. URL: http:\/\/www.cs.ru.nl\/venanzio\/publications\/induction_recursion.pdf , March 2004 . V. Capretta. A Polymorphic Representation of Induction-Recursion. Retrieved 9\/12\/12. URL: http:\/\/www.cs.ru.nl\/venanzio\/publications\/induction_recursion.pdf, March 2004."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086375"},{"key":"e_1_3_2_1_10_1","unstructured":"A. Chlipala. Certified Programming with Dependent Types. http:\/\/adam.chlipala.net\/cpdt\/.  A. Chlipala. Certified Programming with Dependent Types. http:\/\/adam.chlipala.net\/cpdt\/."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596565"},{"key":"e_1_3_2_1_12_1","volume-title":"Thecoq Proof Assistant Reference Manual: Version 8.4","author":"Team Coq Development","year":"2012","unstructured":"Coq Development Team . Thecoq Proof Assistant Reference Manual: Version 8.4 , 2012 . Coq Development Team. Thecoq Proof Assistant Reference Manual: Version 8.4, 2012."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_3_2_1_14_1","volume-title":"Generic Universe Types. In phECOOP","author":"Dietl W.","year":"2007","unstructured":"W. Dietl , S. Drossopoulou , and P. M\u00fcller . Generic Universe Types. In phECOOP , 2007 . W. Dietl, S. Drossopoulou, and P. M\u00fcller. Generic Universe Types. In phECOOP, 2007."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1883978.1884012"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_26"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480922"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/645393.651882"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349328"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384619"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_25_1","volume-title":"Semantics and Logics of Computation, chapter 3.","author":"Hofmann M.","year":"1997","unstructured":"M. Hofmann . Syntax and Semantics of Dependent Types , in Semantics and Logics of Computation, chapter 3. 1997 . M. Hofmann. Syntax and Semantics of Dependent Types, in Semantics and Logics of Computation, chapter 3. 1997."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_27"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1924520.1924527"},{"key":"e_1_3_2_1_30_1","first-page":"12","volume":"8","author":"Militao F.","year":"2012","unstructured":"F. Militao , J. Aldrich , and L. Caires . Rely-Guarantee View Typestate. Retrieved 8\/24 \/ 12 , July 2012 . URL http:\/\/www.cs.cmu.edu\/ foliveir\/papers\/rgviews.pdf. F. Militao, J. Aldrich, and L. Caires. Rely-Guarantee View Typestate. Retrieved 8\/24\/12, July 2012. URL http:\/\/www.cs.cmu.edu\/ foliveir\/papers\/rgviews.pdf.","journal-title":"Rely-Guarantee View Typestate. Retrieved"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103722"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159812"},{"key":"e_1_3_2_1_33_1","volume-title":"ESOP.","author":"Nanevski A.","year":"2007","unstructured":"A. Nanevski , A. Ahmed , G. Morrisett , and L. Birkedal . Abstract Predicates and Mutable ADTs in Hoare Type Theory . In ESOP. 2007 . A. Nanevski, A. Ahmed, G. Morrisett, and L. Birkedal. Abstract Predicates and Mutable ADTs in Hoare Type Theory. In ESOP. 2007."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_3_2_1_35_1","volume-title":"IWACO","author":"Nistor L.","year":"2011","unstructured":"L. Nistor and J. Aldrich . Verifying Object-Oriented Code Using Object Propositions . In IWACO , 2011 . L. Nistor and J. Aldrich. Verifying Object-Oriented Code Using Object Propositions. In IWACO, 2011."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449800"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040326"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/645891.671440"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929553.1929565"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706316"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291156"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094828"},{"key":"e_1_3_2_1_45_1","volume-title":"CONCUR.","author":"Vafeiadis V.","year":"2007","unstructured":"V. Vafeiadis and M. Parkinson . A Marriage of Rely\/Guarantee and Separation Logic . In CONCUR. 2007 . V. Vafeiadis and M. Parkinson. A Marriage of Rely\/Guarantee and Separation Logic. In CONCUR. 2007."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_32"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604150"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287637"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869509"}],"event":{"name":"PLDI '13: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Seattle Washington USA","acronym":"PLDI '13","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491956.2462160","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2491956.2462160","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:28:41Z","timestamp":1750217321000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491956.2462160"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,6,16]]},"references-count":49,"alternative-id":["10.1145\/2491956.2462160","10.1145\/2491956"],"URL":"https:\/\/doi.org\/10.1145\/2491956.2462160","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2499370.2462160","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2013,6,16]]},"assertion":[{"value":"2013-06-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}