{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:55Z","timestamp":1775873695898,"version":"3.50.1"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>Mechanisations of programming language specifications are now increasingly common, providing machine-checked modelling of the specification and verification of desired properties such as type safety. However it is challenging to maintain these mechanisations, particularly in the face of an evolving specification. Existing mechanisations of the W3C WebAssembly (Wasm) standard have so far been able to keep pace as the standard evolves, helped enormously by the W3C Wasm standard\u2019s choice to state the language\u2019s semantics in terms of a fully formal specification. However a substantial incoming extension to Wasm, the 2.0 feature set, motivates the investigation of strategies for more efficient production of the core verification artefacts currently associated with the WasmCert-Coq mechanisation of Wasm.<\/jats:p>\n                  <jats:p>In the classic formalisation of a typed operational semantics as followed by the W3C Wasm standard, both the type system and runtime operational semantics are defined as inductive relations, with associated type soundness properties (progress and preservation) and an independent sound interpreter. We investigate two more efficient strategies for producing these artefacts, which are currently all separately defined by WasmCert-Coq. First, the approach of Kokke, Siek, and Wadler for deriving a sound interpreter from a constructive progress proof \u2014 we show that this approach scales to the W3C Wasm 1.0 standard, but results in an inefficient interpreter in our setting. Second, inspired by results from intrinsically-typed languages, we define a progressful interpreter which uses Coq\u2019s dependent types to certify not only its own soundness, but also the progress property. We show that this interpreter can implement several performance optimisations while maintaining these certifications, which are fully erasable when the interpreter is extracted from Coq. Using this approach, we extend the WasmCert-Coq mechanisation to the significantly larger Wasm 2.0 feature set, discovering and correcting several errors in the expanded specification\u2019s type system.<\/jats:p>","DOI":"10.1145\/3704858","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"627-655","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Progressful Interpreters for Efficient WebAssembly Mechanisation"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-4391-1214","authenticated-orcid":false,"given":"Xiaojia","family":"Rao","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-1220-9200","authenticated-orcid":false,"given":"Stefan","family":"Radziuk","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0596-877X","authenticated-orcid":false,"given":"Conrad","family":"Watt","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4187-0585","authenticated-orcid":false,"given":"Philippa","family":"Gardner","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3636501.3636951"},{"key":"e_1_3_2_3_2","unstructured":"Guillaume Allais. 2017. GitHub - Total Parser Combinators in Coq. https:\/\/github.com\/gallais\/parseque."},{"key":"e_1_3_2_4_2","unstructured":"Guillaume Allais. 2018. Agdarsec-total parser combinators. 45\u201359. Publisher Copyright: \u00a9 JFLA 2018 - Journees Francophones des Langages Applicatifs. All rights reserved. Sylvie Boldo Nicolas Magaud. Journ\u00e9es Francophones des Langages Applicatifs 2018. Sylvie Boldo; Nicolas Magaud. Journ\u00e9es Francophones des Langages Applicatifs 2018 Jan 2018 Banyuls-sur-Mer France. publi\u00e9 par les auteurs 2018. \u3008hal-01707376\u3009; Vingt-neuviemes Journees Francophones des Langages Applicatifs JFLA 2018-29th French-Speaking Conference on Applicative Languages JFLA 2018; Conference date: 24-01-2018 Through 27-01-2018."},{"key":"e_1_3_2_5_2","unstructured":"Bytecode Alliance. [n. d.]. GitHub-bytecodealliance\/wasmtime: A fast and secure runtime for WebAssembly. https:\/\/github.com\/bytecodealliance\/wasmtime. [Accessed 01-07-2024]."},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009866"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158104"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535876"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676982"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-33636-3_10"},{"key":"e_1_3_2_12_2","volume-title":"Certified programming with dependent types: a pragmatic introduction to the Coq proof assistant","author":"Chlipala Adam","year":"2022","unstructured":"Adam Chlipala. 2022. Certified programming with dependent types: a pragmatic introduction to the Coq proof assistant. MIT Press."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2398856.2364546"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429094"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103719"},{"key":"e_1_3_2_16_2","unstructured":"Philip Wadler et al. 1998. The expression problem. http:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/expression\/expression.txt"},{"key":"e_1_3_2_17_2","unstructured":"W3C WebAssembly Community Group. [n. d.]. GitHub - WebAssembly\/spec: WebAssembly specification reference interpreter and test suite. https:\/\/github.com\/WebAssembly\/spec\/tree\/main\/interpreter. [Accessed 09-07-2024]."},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_7"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062363"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503505"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591286"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/2502488.2502491"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102440"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535841"},{"key":"e_1_3_2_26_2","doi-asserted-by":"crossref","unstructured":"Daniel K Lee Karl Crary and Robert Harper. 2007. Towards a mechanized metatheory of Standard ML. In Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 173\u2013184.","DOI":"10.1145\/1190216.1190245"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_28_2","unstructured":"Xavier Leroy Sandrine Blazy Daniel K\u00e4stner Bernhard Schommer Markus Pister and Christian Ferdinand. 2016. CompCert-a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems 8th European Congress."},{"key":"e_1_3_2_29_2","first-page":"200","volume-title":"International Workshop on Types for Proofs and Programs","author":"Letouzey Pierre","year":"2002","unstructured":"Pierre Letouzey. 2002. A new extraction for Coq. In International Workshop on Types for Proofs and Programs. Springer, 200\u2013219."},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69407-6_39"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61055-3_39"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.03.008"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.48456\/tr-453"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_1"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_23"},{"key":"e_1_3_2_36_2","doi-asserted-by":"crossref","unstructured":"Daejun Park Andrei Stef\u0103nescu and Grigore Ro\u015fu. 2015. KJS: A complete formal semantics of JavaScript. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. 346\u2013356.","DOI":"10.1145\/2737924.2737991"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Xiaojia Rao Stefan Radziuk Conrad Watt and Philippa Gardner. 2024. Artifact: Progressful Interpreters for Efficient WebAssembly Mechanisation. https:\/\/doi.org\/10.5281\/zenodo.14052598 10.5281\/zenodo.14052598","DOI":"10.5281\/zenodo.14052598"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_3_2_39_2","unstructured":"Tiark Rompf and Nada Amin. 2016. From F to DOT: Type Soundness Proofs with Definitional Interpreters. arXiv:1510.05216 [cs.PL] https:\/\/arxiv.org\/abs\/1510.05216"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/2428116.2428120"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000229"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563355"},{"key":"e_1_3_2_44_2","unstructured":"Wasm. 2024. WasmCert-Coq: A mechanisation of Wasm in Coq. https:\/\/github.com\/WasmCert\/WasmCert-Coq\/"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3167082"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_4"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591224"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3110275"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656440"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704858","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704858","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:16:40Z","timestamp":1770200200000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704858"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":49,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704858"],"URL":"https:\/\/doi.org\/10.1145\/3704858","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}