{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:37Z","timestamp":1772164057167,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":61,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,1,8]],"date-time":"2014-01-08T00:00:00Z","timestamp":1389139200000},"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":[[2014,1,8]]},"DOI":"10.1145\/2535838.2535876","type":"proceedings-article","created":{"date-parts":[[2014,1,14]],"date-time":"2014-01-14T08:40:06Z","timestamp":1389688806000},"page":"87-100","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":66,"title":["A trusted mechanised JavaScript specification"],"prefix":"10.1145","author":[{"given":"Martin","family":"Bodin","sequence":"first","affiliation":[{"name":"Inria & ENS Lyon, Rennes, France"}]},{"given":"Arthur","family":"Chargueraud","sequence":"additional","affiliation":[{"name":"Inria & LRI, Universite Paris Sud, CNRS, Saclay, France"}]},{"given":"Daniele","family":"Filaretti","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}]},{"given":"Philippa","family":"Gardner","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}]},{"given":"Sergio","family":"Maffeis","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}]},{"given":"Daiva","family":"Naudziuniene","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}]},{"given":"Alan","family":"Schmitt","sequence":"additional","affiliation":[{"name":"Inria, Rennes, France"}]},{"given":"Gareth","family":"Smith","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2014,1,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_25"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11531142_19"},{"key":"e_1_3_2_2_3_1","first-page":"1","volume-title":"ESOP","author":"Appel A. W.","year":"2011","unstructured":"A. W. Appel . Verified software toolchain - (invited talk) . In ESOP , pages 1 -- 17 , 2011 . A. W. Appel. Verified software toolchain - (invited talk). In ESOP, pages 1--17, 2011."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429099"},{"key":"e_1_3_2_2_6_1","volume-title":"USENIX Security Symposium","author":"Bhargavan K.","year":"2013","unstructured":"K. Bhargavan , A. Delignat-Lavaud , and S. Maffeis . Language-based defenses against untrusted browser origins . In USENIX Security Symposium , 2013 . K. Bhargavan, A. Delignat-Lavaud, and S. Maffeis. Language-based defenses against untrusted browser origins. In USENIX Security Symposium, 2013."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111043"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.11.008"},{"key":"e_1_3_2_2_10_1","volume-title":"http:\/\/www.iso.org\/iso\/iso_catalogue\/catalogue_tc\/catalogue_detail.htm?csnumber=57853","author":"IEC","year":"2011","unstructured":"C11. ISO\/ IEC 9899:2011. http:\/\/www.iso.org\/iso\/iso_catalogue\/catalogue_tc\/catalogue_detail.htm?csnumber=57853 , 2011 . C11. ISO\/IEC 9899:2011. http:\/\/www.iso.org\/iso\/iso_catalogue\/catalogue_tc\/catalogue_detail.htm?csnumber=57853, 2011."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_3"},{"key":"e_1_3_2_2_12_1","volume-title":"Dependent types for JavaScript. CoRR, abs\/1112.4106","author":"Chugh R.","year":"2011","unstructured":"R. Chugh and R. Jhala . Dependent types for JavaScript. CoRR, abs\/1112.4106 , 2011 . R. Chugh and R. Jhala. Dependent types for JavaScript. CoRR, abs\/1112.4106, 2011."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542483"},{"key":"e_1_3_2_2_14_1","volume-title":"http:\/\/bisect.x9c.fr\/","author":"Clerc X.","year":"2012","unstructured":"X. Clerc . Bisect. http:\/\/bisect.x9c.fr\/ , 2012 . X. Clerc. Bisect. http:\/\/bisect.x9c.fr\/, 2012."},{"key":"e_1_3_2_2_15_1","volume-title":"http:\/\/compcert.inria.fr\/","author":"Team Compcert","year":"2013","unstructured":"Compcert Team . Compcert. http:\/\/compcert.inria.fr\/ , 2013 . Compcert Team. Compcert. http:\/\/compcert.inria.fr\/, 2013."},{"key":"e_1_3_2_2_16_1","unstructured":"D. Crockford. ADSafe: Making JavaScript safe for advertising. http:\/\/adsafe.org\/ 2007.  D. Crockford. ADSafe: Making JavaScript safe for advertising. http:\/\/adsafe.org\/ 2007."},{"key":"e_1_3_2_2_17_1","volume-title":"Is the Java type system sound? In FOOL4","author":"Drossopoulou S.","year":"1997","unstructured":"S. Drossopoulou and S. Eisenbach . Is the Java type system sound? In FOOL4 , 1997 . S. Drossopoulou and S. Eisenbach. Is the Java type system sound? In FOOL4, 1997."},{"key":"e_1_3_2_2_18_1","volume-title":"http:\/\/test262.ecmascript.org\/","author":"International ECMA","year":"2010","unstructured":"ECMA International . Test262. http:\/\/test262.ecmascript.org\/ , 2010 . ECMA International. Test262. http:\/\/test262.ecmascript.org\/, 2010."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103719"},{"key":"e_1_3_2_2_20_1","first-page":"501","volume-title":"CAV","author":"Farzan A.","year":"2004","unstructured":"A. Farzan , F. Chen , J. Meseguer , and G. Rosu . Formal analysis of Java programs in JavaFAN . In CAV , pages 501 -- 505 , 2004 . A. Farzan, F. Chen, J. Meseguer, and G. Rosu. Formal analysis of Java programs in JavaFAN. In CAV, pages 501--505, 2004."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429114"},{"key":"e_1_3_2_2_22_1","unstructured":"Free Software Foundation. C language testsuites: \"C-torture\" version 4.4.2. http:\/\/gcc.gnu.org\/onlinedocs\/gccint\/C-Tests.html 2010.  Free Software Foundation. C language testsuites: \"C-torture\" version 4.4.2. http:\/\/gcc.gnu.org\/onlinedocs\/gccint\/C-Tests.html 2010."},{"key":"e_1_3_2_2_23_1","volume-title":"Test262 bug 56. https:\/\/bugs.ecmascript.org\/show_bug.cgi?id=56","author":"Fugate D.","year":"2011","unstructured":"D. Fugate . Test262 bug 56. https:\/\/bugs.ecmascript.org\/show_bug.cgi?id=56 , 2011 . D. Fugate. Test262 bug 56. https:\/\/bugs.ecmascript.org\/show_bug.cgi?id=56, 2011."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103663"},{"key":"e_1_3_2_2_25_1","volume-title":"The Closure Compiler. https:\/\/developers.google.com\/closure\/compiler\/","author":"Google Inc.","year":"2009","unstructured":"Google Inc. The Closure Compiler. https:\/\/developers.google.com\/closure\/compiler\/ , 2009 . Google Inc. The Closure Compiler. https:\/\/developers.google.com\/closure\/compiler\/, 2009."},{"key":"e_1_3_2_2_26_1","first-page":"151","volume-title":"USENIX Security Symposium","author":"Guarnieri S.","year":"2009","unstructured":"S. Guarnieri and V. B. Livshits . GATEKEEPER: Mostly static enforcement of security and reliability policies for JavaScript code . In USENIX Security Symposium , pages 151 -- 168 , 2009 . S. Guarnieri and V. B. Livshits. GATEKEEPER: Mostly static enforcement of security and reliability policies for JavaScript code. In USENIX Security Symposium, pages 151--168, 2009."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001442"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1883978.1883988"},{"key":"e_1_3_2_2_29_1","first-page":"423","volume-title":"IFIP Congress (1)","author":"Gurevich Y.","year":"1994","unstructured":"Y. Gurevich . Evolving algebras. In IFIP Congress (1) , pages 423 -- 427 , 1994 . Y. Gurevich. Evolving algebras. In IFIP Congress (1), pages 423--427, 1994."},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.19"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292535.1292543"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1529282.1529711"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_17"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190245"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.11"},{"key":"e_1_3_2_2_36_1","unstructured":"S. Maffeis J. Mitchell and A. Taly. ECMA 262-3 operational semantics. http:\/\/jssec.net\/semantics\/ 2007.  S. Maffeis J. Mitchell and A. Taly. ECMA 262-3 operational semantics. http:\/\/jssec.net\/semantics\/ 2007."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89330-1_22"},{"key":"e_1_3_2_2_38_1","volume-title":"ESORICS'09","author":"Maffeis S.","year":"2009","unstructured":"S. Maffeis , J. Mitchell , and A. Taly . Isolating JavaScript with filters, rewriting, and wrappers . In ESORICS'09 . Springer , 2009 . S. Maffeis, J. Mitchell, and A. Taly. Isolating JavaScript with filters, rewriting, and wrappers. In ESORICS'09. Springer, 2009."},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.16"},{"key":"e_1_3_2_2_40_1","volume-title":"http:\/\/flocq.gforge.inria.fr\/","author":"Melquiond G.","year":"2012","unstructured":"G. Melquiond . Floats for Coq 2.1.0. http:\/\/flocq.gforge.inria.fr\/ , 2012 . G. Melquiond. Floats for Coq 2.1.0. http:\/\/flocq.gforge.inria.fr\/, 2012."},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/549659"},{"key":"e_1_3_2_2_42_1","volume-title":"Mozilla automated JavaScript tests. https:\/\/developer.mozilla.org\/en-US\/docs\/SpiderMonkey\/Running_Automated_JavaScript_Tests","year":"2013","unstructured":"Mozilla. Mozilla automated JavaScript tests. https:\/\/developer.mozilla.org\/en-US\/docs\/SpiderMonkey\/Running_Automated_JavaScript_Tests , 2013 . Mozilla. Mozilla automated JavaScript tests. https:\/\/developer.mozilla.org\/en-US\/docs\/SpiderMonkey\/Running_Automated_JavaScript_Tests, 2013."},{"key":"e_1_3_2_2_43_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L. C. Paulson , and M. Wenzel . Isabelle\/HOL - A Proof Assistant for Higher-Order Logic , volume 2283 of Lecture Notes in Computer Science . Springer , 2002 . T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle\/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002."},{"key":"e_1_3_2_2_44_1","unstructured":"M. Norrish. Formalising C in HOL. PhD thesis Computer Lab. University of Cambridge 1998.  M. Norrish. Formalising C in HOL. PhD thesis Computer Lab. University of Cambridge 1998."},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1533057.1533067"},{"key":"e_1_3_2_2_46_1","volume-title":"FOOL","author":"Park C.","year":"2011","unstructured":"C. Park , H. Lee , and S. Ryu . An empirical study on the rewritability of the with statement in JavaScript . In FOOL , 2011 . C. Park, H. Lee, and S. Ryu. An empirical study on the rewritability of the with statement in JavaScript. In FOOL, 2011."},{"key":"e_1_3_2_2_47_1","volume-title":"FOOL","author":"Park C.","year":"2012","unstructured":"C. Park , H. Lee , and S. Ryu . SAFE: Formal specification and implementation of a scalable analysis framewrok for ECMAscript . In FOOL , 2012 . C. Park, H. Lee, and S. Ryu. SAFE: Formal specification and implementation of a scalable analysis framewrok for ECMAscript. In FOOL, 2012."},{"key":"e_1_3_2_2_48_1","first-page":"202","volume-title":"CADE","author":"Pfenning F.","year":"1999","unstructured":"F. Pfenning and C. Sch\u00fcrmann . System description: Twelf - a metalogical framework for deductive systems . In CADE , pages 202 -- 206 , 1999 . F. Pfenning and C. Sch\u00fcrmann. System description: Twelf - a metalogical framework for deductive systems. In CADE, pages 202--206, 1999."},{"key":"e_1_3_2_2_49_1","volume-title":"USENIX Security Symposium","author":"Politz J. G.","year":"2011","unstructured":"J. G. Politz , S. A. Eliopoulos , A. Guha , and S. Krishnamurthi . ADsafety: Type-based verification of JavaScript sandboxing . In USENIX Security Symposium , 2011 . J. G. Politz, S. A. Eliopoulos, A. Guha, and S. Krishnamurthi. ADsafety: Type-based verification of JavaScript sandboxing. In USENIX Security Symposium, 2011."},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480360.2384579"},{"key":"e_1_3_2_2_51_1","unstructured":"J. G. Politz B. S. Lerner H. Q. de la Vallee T. Nelson A. Guha M. Carroll and S. Krishnamurthi. Mechanized \u03bbJS. http:\/\/blog.brownplt.org\/2012\/06\/04\/lambdajs-coq.html 2012.  J. G. Politz B. S. Lerner H. Q. de la Vallee T. Nelson A. Guha M. Carroll and S. Krishnamurthi. Mechanized \u03bbJS. http:\/\/blog.brownplt.org\/2012\/06\/04\/lambdajs-coq.html 2012."},{"key":"e_1_3_2_2_52_1","first-page":"52","volume-title":"ECOOP'11","author":"Richards G.","year":"2011","unstructured":"G. Richards , C. Hammer , B. Burg , and J. Vitek . The eval that men do - A large-scale study of the use of eval in JavaScript applications . In ECOOP'11 , pages 52 -- 78 . Springer , 2011 . G. Richards, C. Hammer, B. Burg, and J. Vitek. The eval that men do - A large-scale study of the use of eval in JavaScript applications. In ECOOP'11, pages 52--78. Springer, 2011."},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_3_2_2_54_1","volume-title":"https:\/\/hg.mozilla.org\/mozilla-central\/rev\/5593cd83590e","author":"Schneidereit T.","year":"2012","unstructured":"T. Schneidereit . Convert some array extras to self-hosted js implementations. https:\/\/hg.mozilla.org\/mozilla-central\/rev\/5593cd83590e , 2012 . T. Schneidereit. Convert some array extras to self-hosted js implementations. https:\/\/hg.mozilla.org\/mozilla-central\/rev\/5593cd83590e, 2012."},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"key":"e_1_3_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/645580.658814"},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.39"},{"key":"e_1_3_2_2_58_1","unstructured":"The JSCert Team. Mozilla Bug 862771 V8 Issue 2529 ES6 Bugs 1442-1444 Test262 Bug 1445 1450 1600. https:\/\/bugzilla.mozilla.org\/show_bug.cgi?id=862771 http:\/\/code.google.com\/p\/v8\/issues\/detail?id=2529 https:\/\/bugs.ecmascript.org\/show_bug.cgi?id={1442-1445 1450 1600} 2013.  The JSCert Team. Mozilla Bug 862771 V8 Issue 2529 ES6 Bugs 1442-1444 Test262 Bug 1445 1450 1600. https:\/\/bugzilla.mozilla.org\/show_bug.cgi?id=862771 http:\/\/code.google.com\/p\/v8\/issues\/detail?id=2529 https:\/\/bugs.ecmascript.org\/show_bug.cgi?id={1442-1445 1450 1600} 2013."},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_28"},{"key":"e_1_3_2_2_60_1","volume-title":"Test262 and browsers. https:\/\/bugs.webkit.org\/show_bug.cgi?id={38970,104309} http:\/\/code.google.com\/p\/v8\/issues\/detail?id={705,2446} https:\/\/bugzilla.mozilla.org\/show_bug.cgi?id=819125","author":"Various","year":"2010","unstructured":"Various developers. Bugs in ES6 , Test262 and browsers. https:\/\/bugs.webkit.org\/show_bug.cgi?id={38970,104309} http:\/\/code.google.com\/p\/v8\/issues\/detail?id={705,2446} https:\/\/bugzilla.mozilla.org\/show_bug.cgi?id=819125 , 2010 --2012. Various developers. Bugs in ES6, Test262 and browsers. https:\/\/bugs.webkit.org\/show_bug.cgi?id={38970,104309} http:\/\/code.google.com\/p\/v8\/issues\/detail?id={705,2446} https:\/\/bugzilla.mozilla.org\/show_bug.cgi?id=819125, 2010--2012."},{"key":"e_1_3_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926393"}],"event":{"name":"POPL '14: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"San Diego California USA","acronym":"POPL '14","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2535838.2535876","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2535838.2535876","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:10:06Z","timestamp":1750219806000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2535838.2535876"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1,8]]},"references-count":61,"alternative-id":["10.1145\/2535838.2535876","10.1145\/2535838"],"URL":"https:\/\/doi.org\/10.1145\/2535838.2535876","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2578855.2535876","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2014,1,8]]},"assertion":[{"value":"2014-01-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}