{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:48Z","timestamp":1775790768046,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":37,"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.2491978","type":"proceedings-article","created":{"date-parts":[[2013,6,11]],"date-time":"2013-06-11T12:03:50Z","timestamp":1370952230000},"page":"387-398","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":64,"title":["Verifying higher-order programs with the dijkstra monad"],"prefix":"10.1145","author":[{"given":"Nikhil","family":"Swamy","sequence":"first","affiliation":[{"name":"Microsoft Research, Redmond, WA, USA"}]},{"given":"Joel","family":"Weinberger","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, CA, USA"}]},{"given":"Cole","family":"Schlesinger","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, NJ, USA"}]},{"given":"Juan","family":"Chen","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA, USA"}]},{"given":"Benjamin","family":"Livshits","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA, USA"}]}],"member":"320","published-online":{"date-parts":[[2013,6,16]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"3","article-title":"Verification of object-oriented programs with invariants","author":"Barnett M.","year":"2004","unstructured":"M. Barnett , R. DeLine , M. Fahndrich , K. R. M. Leino , and W. Schulte . Verification of object-oriented programs with invariants . JOT , 3 , 2004 . M. Barnett, R. DeLine, M. Fahndrich, K. R. M. Leino, and W. Schulte. Verification of object-oriented programs with invariants. JOT, 3, 2004.","journal-title":"JOT"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1947873.1947880"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863560"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929529.1929532"},{"key":"e_1_3_2_1_6_1","volume-title":"Garland Publishing","author":"Cartwright R.","year":"1976","unstructured":"R. Cartwright . A Practical Formal Semantic Definition and Verification System for TYPED LISP . Garland Publishing , New York , 1976 . R. Cartwright. A Practical Formal Semantic Definition and Verification System for TYPED LISP. Garland Publishing, New York, 1976."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113469"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034828"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806643"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384659"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103686"},{"key":"e_1_3_2_1_12_1","volume-title":"JavaScript: The Good Parts","author":"Crockford D.","year":"2008","unstructured":"D. Crockford . JavaScript: The Good Parts . O'Reilly Media Inc ., 2008 . D. Crockford. JavaScript: The Good Parts. O'Reilly Media Inc., 2008."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_1_15_1","first-page":"173","volume-title":"CAV","author":"Filli\u00e2tre J.-C.","year":"2007","unstructured":"J.-C. Filli\u00e2tre and C. March\u00e9 . The why\/krakatoa\/caduceus platform for deductive program verification . In CAV , pages 173 -- 177 , 2007 . J.-C. Filli\u00e2tre and C. March\u00e9. The why\/krakatoa\/caduceus platform for deductive program verification. In CAV, pages 173--177, 2007."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429114"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1376916.1376953"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103663"},{"key":"e_1_3_2_1_19_1","volume-title":"USENIX Security","author":"Guarnieri S.","year":"2009","unstructured":"S. Guarnieri and B. Livshits . Gatekeeper: Mostly static enforcement of security and reliability policies for JavaScript code . In USENIX Security , 2009 . S. Guarnieri and B. Livshits. Gatekeeper: Mostly static enforcement of security and reliability policies for JavaScript code. In USENIX Security, 2009."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1883978.1883988"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.36"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00004-2"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224203"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_17"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_26"},{"key":"e_1_3_2_1_28_1","first-page":"21","volume-title":"IFIP Congress","author":"McCarthy J.","year":"1962","unstructured":"J. McCarthy . Towards a mathematical science of computation . In IFIP Congress , pages 21 -- 28 , 1962 . J. McCarthy. Towards a mathematical science of computation. In IFIP Congress, pages 21--28, 1962."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1762174.1762194"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964024"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040326"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034778"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863561"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:3)2011"}],"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.2491978","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2491956.2491978","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:39:10Z","timestamp":1750221550000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491956.2491978"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,6,16]]},"references-count":37,"alternative-id":["10.1145\/2491956.2491978","10.1145\/2491956"],"URL":"https:\/\/doi.org\/10.1145\/2491956.2491978","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2499370.2491978","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"}}]}}