{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T22:33:48Z","timestamp":1769726028683,"version":"3.49.0"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030908690","type":"print"},{"value":"9783030908706","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-90870-6_4","type":"book-chapter","created":{"date-parts":[[2021,11,10]],"date-time":"2021-11-10T00:06:44Z","timestamp":1636502804000},"page":"61-79","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Two Mechanisations of WebAssembly 1.0"],"prefix":"10.1007","author":[{"given":"Conrad","family":"Watt","sequence":"first","affiliation":[]},{"given":"Xiaojia","family":"Rao","sequence":"additional","affiliation":[]},{"given":"Jean","family":"Pichon-Pharabod","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Bodin","sequence":"additional","affiliation":[]},{"given":"Philippa","family":"Gardner","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,11,10]]},"reference":[{"key":"4_CR1","unstructured":"Allais, G.: Parseque (2017). https:\/\/github.com\/gallais\/parseque"},{"key":"4_CR2","unstructured":"Allais, G.: Agdarsec - total parser combinators. In: JFLA 2018 (2018)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-662-46669-8_12","volume-title":"Programming Languages and Systems","author":"M Batty","year":"2015","unstructured":"Batty, M., Memarian, K., Nienhuis, K., Pichon-Pharabod, J., Sewell, P.: The problem of programming language concurrency semantics. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 283\u2013307. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_12"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. J. Autom. Reason. 43(3), 263\u2013288 (2009). https:\/\/doi.org\/10.1007\/s10817-009-9148-3. https:\/\/hal.inria.fr\/inria-00352524","DOI":"10.1007\/s10817-009-9148-3"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Bodin, M., et al.: A trusted mechanised JavaScript specification. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 87\u2013100. Association for Computing Machinery, New York (2014). https:\/\/doi.org\/10.1145\/2535838.2535876","DOI":"10.1145\/2535838.2535876"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Bogdanas, D., Ro\u015fu, G.: K-Java: a complete semantics of Java. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, pp. 445\u2013456. Association for Computing Machinery, New York (2015). https:\/\/doi.org\/10.1145\/2676726.2676982","DOI":"10.1145\/2676726.2676982"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Boldo, S., Jourdan, J.H., Leroy, X., Melquiond, G.: Verified compilation of floating-point computations. J. Autom. Reason. 54(2), 135\u2013163 (2015). http:\/\/xavierleroy.org\/publi\/floating-point-compcert.pdf","DOI":"10.1007\/s10817-014-9317-x"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Boldo, S., Melquiond, G.: Flocq: A unified library for proving floating-point algorithms in coq. In: 2011 IEEE 20th Symposium on Computer Arithmetic, pp. 243\u2013252 (2011). https:\/\/doi.org\/10.1109\/ARITH.2011.40","DOI":"10.1109\/ARITH.2011.40"},{"key":"4_CR9","unstructured":"Bynens, M.: Loading webassembly modules efficiently (2018). https:\/\/developers.google.com\/web\/updates\/2018\/04\/loading-wasm"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, pp. 533\u2013544. Association for Computing Machinery, New York (2012). https:\/\/doi.org\/10.1145\/2103656.2103719","DOI":"10.1145\/2103656.2103719"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1007\/978-3-662-44202-9_23","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"D Filaretti","year":"2014","unstructured":"Filaretti, D., Maffeis, S.: An executable formal semantics of PHP. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 567\u2013592. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44202-9_23"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Fragoso Santos, J., Maksimovi\u0107, P., Sampaio, G., Gardner, P.: Javert 2.0: compositional symbolic execution for javascript. Proc. ACM Program. Lang. 3(POPL) (2019). https:\/\/doi.org\/10.1145\/3290379","DOI":"10.1145\/3290379"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-14107-2_7","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"A Guha","year":"2010","unstructured":"Guha, A., Saftoiu, C., Krishnamurthi, S.: The essence of JavaScript. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 126\u2013150. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14107-2_7"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Haas, A., et al.: Bringing the web up to speed with WebAssembly. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM (2017)","DOI":"10.1145\/3062341.3062363"},{"key":"4_CR15","unstructured":"Huang, X.: A mechanized formalization of the webassembly specification in coq. In: RIT Computer Science (2019)"},{"key":"4_CR16","unstructured":"Hupel, L., Zhang, Y.: Cakeml. Archive of Formal Proofs, March 2018. https:\/\/isa-afp.org\/entries\/CakeML.html. Formal proof development"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018)","DOI":"10.1017\/S0956796818000151"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst. 28(4), 619\u2013695 (2006). https:\/\/doi.org\/10.1145\/1146809.1146811","DOI":"10.1145\/1146809.1146811"},{"key":"4_CR19","doi-asserted-by":"publisher","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 179\u2013191. Association for Computing Machinery, New York (2014). https:\/\/doi.org\/10.1145\/2535838.2535841","DOI":"10.1145\/2535838.2535841"},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Principles of Programming Languages (POPL), pp. 179\u2013191. ACM Press (2014). https:\/\/doi.org\/10.1145\/2535838.2535841. https:\/\/cakeml.org\/popl14.pdf","DOI":"10.1145\/2535838.2535841"},{"key":"4_CR21","doi-asserted-by":"publisher","unstructured":"Lee, D.K., Crary, K., Harper, R.: Towards a mechanized metatheory of standard ML. In: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, pp. 173\u2013184. Association for Computing Machinery, New York (2007). https:\/\/doi.org\/10.1145\/1190216.1190245","DOI":"10.1145\/1190216.1190245"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-44585-4_26","volume-title":"Computer Aided Verification","author":"X Leroy","year":"2001","unstructured":"Leroy, X.: Java bytecode verification: an overview. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 265\u2013285. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_26"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","DOI":"10.1145\/1538788.1538814"},{"key":"4_CR24","doi-asserted-by":"publisher","unstructured":"Memarian, K., et al.: Into the depths of C: elaborating the de facto standards. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, pp. 1\u201315. Association for Computing Machinery, New York (2016). https:\/\/doi.org\/10.1145\/2908080.2908081","DOI":"10.1145\/2908080.2908081"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Mulligan, D.P., Owens, S., Gray, K.E., Ridge, T., Sewell, P.: Lem: reusable engineering of real-world semantics. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP 2014, pp. 175\u2013188. ACM, New York (2014). https:\/\/doi.org\/10.1145\/2628136.2628143","DOI":"10.1145\/2628136.2628143"},{"key":"4_CR26","unstructured":"Norrish, M.: C formalised in HOL. Technical report (1998)"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-78739-6_1","volume-title":"Programming Languages and Systems","author":"S Owens","year":"2008","unstructured":"Owens, S.: A sound semantics for OCamllight. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 1\u201315. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78739-6_1"},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"Park, D., Stef\u0103nescu, A., Ro\u015fu, G.: KJS: A complete formal semantics of JavaScript. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pp. 346\u2013356. Association for Computing Machinery, New York (2015). https:\/\/doi.org\/10.1145\/2737924.2737991","DOI":"10.1145\/2737924.2737991"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction \u2014 CADE-16","author":"F Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: twelf \u2014 a meta-logical framework for deductive systems. In: CADE 1999. LNCS (LNAI), vol. 1632, pp. 202\u2013206. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48660-7_14"},{"key":"4_CR30","unstructured":"Pierce, B.C.: Types and Programming Languages, 1st edn. The MIT Press, Cambridge (2002)"},{"key":"4_CR31","doi-asserted-by":"publisher","unstructured":"Ringer, T., Palmskog, K., Sergey, I., Gligoric, M., Tatlock, Z.: QED at large: a survey of engineering of formally verified software. Found. Trends Program. Lang. 5(2-3), 102\u2013281 (2019). https:\/\/doi.org\/10.1561\/2500000045","DOI":"10.1561\/2500000045"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Rou, G., erb\u0103nut\u0103, T.F.: An overview of the K semantic framework. J. Logic Algebraic Program. 79(6), 397\u2013434 (2010). https:\/\/doi.org\/10.1016\/j.jlap.2010.03.012. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S1567832610000160. Membrane computing and programming","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"4_CR33","doi-asserted-by":"publisher","unstructured":"Santos, J.F., Maksimovi\u0107, P., Grohens, T., Dolby, J., Gardner, P.: Symbolic execution for JavaScript. In: Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018. Association for Computing Machinery, New York (2018). https:\/\/doi.org\/10.1145\/3236950.3236956","DOI":"10.1145\/3236950.3236956"},{"key":"4_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/3-540-48737-9_3","volume-title":"Formal Syntax and Semantics of Java","author":"D Syme","year":"1999","unstructured":"Syme, D.: Proving Java type soundness. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol. 1523, pp. 83\u2013118. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48737-9_3"},{"key":"4_CR35","doi-asserted-by":"publisher","unstructured":"Tan, Y.K., Owens, S., Kumar, R.: A verified type system for CakeML. In: Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages. IFL 2015. Association for Computing Machinery, New York (2015). https:\/\/doi.org\/10.1145\/2897336.2897344","DOI":"10.1145\/2897336.2897344"},{"key":"4_CR36","unstructured":"WasmCert: WasmCert (2021). https:\/\/github.com\/WasmCert"},{"key":"4_CR37","doi-asserted-by":"publisher","unstructured":"Watt, C.: Mechanising and verifying the WebAssembly specification. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pp. 53\u201365. Association for Computing Machinery, New York (2018). https:\/\/doi.org\/10.1145\/3167082","DOI":"10.1145\/3167082"},{"key":"4_CR38","unstructured":"Watt, C.: Mechanising and evolving the formal semantics of WebAssembly: The Web\u2019s new low-level language (2021, not yet published)"},{"key":"4_CR39","unstructured":"WebAssembly Community Group: tests (2020). https:\/\/github.com\/WebAssembly\/spec\/tree\/704d9d9e9c861fdb957c3d5e928f1d046a31497e\/test"},{"key":"4_CR40","unstructured":"WebAssembly Community Group: Webassembly (2020). https:\/\/github.com\/WebAssembly\/spec\/tree\/704d9d9e9c861fdb957c3d5e928f1d046a31497e\/"},{"key":"4_CR41","unstructured":"WebAssembly Community Group: bulk-memory-operations (2021). https:\/\/github.com\/WebAssembly\/bulk-memory-operations"},{"key":"4_CR42","unstructured":"WebAssembly Community Group: GC (2021). https:\/\/github.com\/WebAssembly\/gc"},{"key":"4_CR43","unstructured":"WebAssembly Working Group: Binary format (2019). https:\/\/www.w3.org\/TR\/2019\/REC-wasm-core-1-20191205\/#binary-format%E2%91%A0"},{"key":"4_CR44","unstructured":"WebAssembly Working Group: Instantiation (2019). https:\/\/www.w3.org\/TR\/2019\/REC-wasm-core-1-20191205\/#instantiation%E2%91%A1"},{"key":"4_CR45","unstructured":"WebAssembly Working Group: Webassembly core specification (2019). https:\/\/www.w3.org\/TR\/2019\/REC-wasm-core-1-20191205\/"},{"key":"4_CR46","doi-asserted-by":"publisher","unstructured":"Wright, A., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38\u201394 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1093","DOI":"10.1006\/inco.1994.1093"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-90870-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,10]],"date-time":"2021-11-10T00:08:08Z","timestamp":1636502888000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-90870-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030908690","9783030908706"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-90870-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"10 November 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 November 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 November 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/formalmethods2021.csp.escience.cn\/dct\/page\/1","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"131","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Additionally, this includes 4 invited full papers.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}