{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:48:05Z","timestamp":1772164085472,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":71,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["25280024,15H05706"],"award-info":[{"award-number":["25280024,15H05706"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1145\/3009837.3009875","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"530-544","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Stateful manifest contracts"],"prefix":"10.1145","author":[{"given":"Taro","family":"Sekiyama","sequence":"first","affiliation":[{"name":"IBM Research, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Atsushi","family":"Igarashi","sequence":"additional","affiliation":[{"name":"Kyoto University, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73561"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_17"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987211.1987213"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/2033939.2033946"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863560"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806005971"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.469460"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.3112"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364539"},{"key":"e_1_3_2_2_10_1","first-page":"58","volume-title":"Analysis and Verification","author":"Clarke D.","unstructured":"D. Clarke , J. \u00d6stlund , I. Sergey , and T. Wrigstad . Ownership types: A survey. In Aliasing in Object-Oriented Programming. Types , Analysis and Verification , pages 15\u2013 58 . 2013.. D. Clarke, J. \u00d6stlund, I. Sergey, and T. Wrigstad. Ownership types: A survey. In Aliasing in Object-Oriented Programming. Types, Analysis and Verification, pages 15\u201358. 2013.."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286947"},{"key":"e_1_3_2_2_12_1","first-page":"318","volume-title":"Analysis and Verification","author":"Dietl W.","unstructured":"W. Dietl and P. M\u00fcller . Object ownership in program verification. In Aliasing in Object-Oriented Programming. Types , Analysis and Verification , pages 289\u2013 318 . 2013.. W. Dietl and P. M\u00fcller. Object ownership in program verification. In Aliasing in Object-Oriented Programming. Types, Analysis and Verification, pages 289\u2013318. 2013.."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_11"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034800"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604151"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85373-2_7"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111059"},{"key":"e_1_3_2_2_19_1","volume-title":"ACM FOOL\/WOOD","author":"Flanagan C.","year":"2006","unstructured":"C. Flanagan , S. N. Freund , and A. Tomb . Hybrid types, invariants, and refinements for imperative objects . In ACM FOOL\/WOOD , 2006 . C. Flanagan, S. N. Freund, and A. Tomb. Hybrid types, invariants, and refinements for imperative objects. In ACM FOOL\/WOOD, 2006."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462160"},{"key":"e_1_3_2_2_21_1","unstructured":"M. Greenberg. Manifest Contracts. PhD thesis University of Pennsylvania 2013.   M. Greenberg. Manifest Contracts. PhD thesis University of Pennsylvania 2013."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706341"},{"key":"e_1_3_2_2_23_1","first-page":"104","volume-title":"Scheme and Functional Programming Workshop","author":"Gronski J.","year":"2006","unstructured":"J. Gronski , K. Knowles , A. Tomb , S. N. Freund , and C. Flanagan . Sage: Hybrid checking for flexible specifications . In Scheme and Functional Programming Workshop , pages 93\u2013 104 , 2006 . J. Gronski, K. Knowles, A. Tomb, S. N. Freund, and C. Flanagan. Sage: Hybrid checking for flexible specifications. In Scheme and Functional Programming Workshop, pages 93\u2013104, 2006."},{"key":"e_1_3_2_2_24_1","first-page":"18","volume-title":"Trends in Functional Prog. (TFP)","author":"Herman D.","year":"2007","unstructured":"D. Herman , A. Tomb , and C. Flanagan . Space-efficient gradual typing . In Trends in Functional Prog. (TFP) , pages 1\u2013 18 , 2007 . D. Herman, A. Tomb, and C. Flanagan. Space-efficient gradual typing. In Trends in Functional Prog. (TFP), pages 1\u201318, 2007."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_15"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_19"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0152-5"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481848.1481853"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73564"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/TEC.1960.5221603"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/534929"},{"key":"e_1_3_2_2_34_1","unstructured":"Microsoft Corporation. TypeScript language specification.  Microsoft Corporation. TypeScript language specification."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77353"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159812"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/1762174.1762194"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628156"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/1-4020-8141-3_34"},{"key":"e_1_3_2_2_43_1","first-page":"406","volume-title":"Analysis and Verification","author":"Parkinson M. J.","unstructured":"M. J. Parkinson and G. M. Bierman . Separation logic for objectoriented programming. In Aliasing in Object-Oriented Programming. Types , Analysis and Verification , pages 366\u2013 406 . 2013.. M. J. Parkinson and G. M. Bierman. Separation logic for objectoriented programming. In Aliasing in Object-Oriented Programming. Types, Analysis and Verification, pages 366\u2013406. 2013.."},{"key":"e_1_3_2_2_44_1","volume-title":"The MIT Press","author":"Pierce B. C.","year":"2002","unstructured":"B. C. Pierce . Types and Programming Languages . The MIT Press , 2002 . B. C. Pierce. Types and Programming Languages. The MIT Press, 2002."},{"key":"e_1_3_2_2_45_1","first-page":"74","volume-title":"Proc. of LICS","author":"Reynolds J. C.","year":"2002","unstructured":"J. C. Reynolds . Separation logic : A logic for shared mutable data structures . In Proc. of LICS , pages 55\u2013 74 , 2002 . J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proc. of LICS, pages 55\u201374, 2002."},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73562"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676996"},{"key":"e_1_3_2_2_49_1","volume-title":"Polymorphic manifest contracts, revised and resolved","author":"Sekiyama T.","year":"2016","unstructured":"T. Sekiyama , A. Igarashi , and M. Greenberg . Polymorphic manifest contracts, revised and resolved , 2016 . Submitted for publication. T. Sekiyama, A. Igarashi, and M. Greenberg. Polymorphic manifest contracts, revised and resolved, 2016. Submitted for publication."},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_18"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_8"},{"key":"e_1_3_2_2_52_1","first-page":"442","volume-title":"Analysis and Verification","author":"Smans J.","unstructured":"J. Smans , B. Jacobs , and F. Piessens . VeriFast for Java: A tutorial. In Aliasing in Object-Oriented Programming. Types , Analysis and Verification , pages 407\u2013 442 . 2013.. J. Smans, B. Jacobs, and F. Piessens. VeriFast for Java: A tutorial. In Aliasing in Object-Oriented Programming. Types, Analysis and Verification, pages 407\u2013442. 2013.."},{"key":"e_1_3_2_2_53_1","volume-title":"Lectures on the Curry-Howard Isomorphism","author":"S\u00f8rensen M. H.","year":"2006","unstructured":"M. H. S\u00f8rensen and U. Pawel . Lectures on the Curry-Howard Isomorphism , Volume 149 (Studies in Logic and the Foundations of Mathematics). Elsevier , New York, NY, USA, 2006 . ISBN 0444520775. M. H. S\u00f8rensen and U. Pawel. Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics). Elsevier, New York, NY, USA, 2006. ISBN 0444520775."},{"key":"e_1_3_2_2_54_1","first-page":"112","volume-title":"Contracts for first-class classes","author":"Strickland T. S.","year":"2010","unstructured":"T. S. Strickland and M. Felleisen . Contracts for first-class classes . pages 97\u2013 112 , 2010 . T. S. Strickland and M. Felleisen. Contracts for first-class classes. pages 97\u2013112, 2010."},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384685"},{"key":"e_1_3_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_14"},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384655"},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.177855"},{"key":"e_1_3_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_29"},{"key":"e_1_3_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"e_1_3_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908110"},{"key":"e_1_3_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143169"},{"key":"e_1_3_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"e_1_3_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/601775.601776"},{"key":"e_1_3_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_2_2_68_1","first-page":"408","volume-title":"TYPES","author":"Xi H.","year":"2003","unstructured":"H. Xi . Applied type system: Extended abstract . In TYPES , pages 394\u2013 408 , 2003 . H. Xi. Applied type system: Extended abstract. In TYPES, pages 394\u2013 408, 2003."},{"key":"e_1_3_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006216"},{"key":"e_1_3_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_3_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103746.2103767"},{"key":"e_1_3_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480889"}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009875","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009875","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:05:33Z","timestamp":1750259133000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009875"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":71,"alternative-id":["10.1145\/3009837.3009875","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009875","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009875","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"2017-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}