{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T03:16:04Z","timestamp":1782875764175,"version":"3.54.5"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000038","name":"NSERC","doi-asserted-by":"crossref","award":["RGPIN-2019-0420"],"award-info":[{"award-number":["RGPIN-2019-0420"]}],"id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n                    We present Wasm-precheck, a superset of WebAssembly (Wasm) that uses indexed types to express and check simple constraints over program values. This additional static reasoning enables safely removing dynamic safety checks from Wasm, such as memory bounds checks. We implement Wasm-precheck as an extension of the Wasmtime compiler and runtime, evaluate the run-time and compile-time performance of Wasm-precheck vs Wasm configurations with explicit dynamic checks, and find an average run-time performance gain of\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:mn>1.71<\/mml:mn>\n                          <mml:mtext>x<\/mml:mtext>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    faster in the widely used PolyBenchC benchmark suite, for a small overhead in binary size (\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:mn>7.18<\/mml:mn>\n                          <mml:mtext>%<\/mml:mtext>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    larger) and type-checking time (1.4% slower). We also prove type and memory safety of Wasm-precheck, prove Wasm safely embeds into Wasm-precheck ensuring backwards compatibility, prove Wasm-precheck type-erases to Wasm, and discuss design and implementation trade-offs.\n                  <\/jats:p>","DOI":"10.1145\/3632922","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T15:48:51Z","timestamp":1704469731000},"page":"2395-2424","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Indexed Types for a Statically Safe WebAssembly"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-8137-7577","authenticated-orcid":false,"given":"Adam T.","family":"Geller","sequence":"first","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-7024-7331","authenticated-orcid":false,"given":"Justine","family":"Frank","sequence":"additional","affiliation":[{"name":"University of Maryland, College Park, USA"},{"name":"University of British Columbia, Vancouver, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6402-4840","authenticated-orcid":false,"given":"William J.","family":"Bowman","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","unstructured":"Bytecode Alliance. 2019. Wasmtime: A fast and secure runtime for WebAssembly. https:\/\/wasmtime.dev\/. Accessed: 2023-06-29."},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384659"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451141"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_1_6_1","unstructured":"Emscripten Contributors. 2015. emscripten. https:\/\/emscripten.org\/. xAccessed: 2023-06-29."},{"key":"e_1_3_1_7_1","author":"Felleisen Matthias","year":"2009","unstructured":"Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. 2009. Semantics engineering with PLT Redex. https:\/\/redex.racketlang.org\/","journal-title":"Semantics engineering with PLT Redex"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/647540.730008"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","unstructured":"Adam T. Geller Justine Frank and William J. Bowman. 2023. Indexed Types for a Statically Safe WebAssembly Artifact. https:\/\/doi.org\/10.1145\/3580426 10.1145\/3580426","DOI":"10.1145\/3580426"},{"key":"e_1_3_1_10_1","article-title":"VectorVisor: A Binary Translation Scheme for Throughput-Oriented GPU Acceleration","author":"Ginzburg Samuel","year":"2023","unstructured":"Samuel Ginzburg, Mohammad Shahrad, and Michael J. Freedman. 2023. VectorVisor: A Binary Translation Scheme for Throughput-Oriented GPU Acceleration. In USENIX Annual Technical Conference (USENIX ATC). https:\/\/www.usenix. org\/conference\/atc23\/presentation\/ginzburg","journal-title":"In USENIX Annual Technical Conference (USENIX ATC)"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062363"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/3358807"},{"key":"e_1_3_1_13_1","author":"Jhala Ranjit","year":"2020","unstructured":"Ranjit Jhala and Niki Vazou. 2020. Refinement Types: A Tutorial. (2020). arXiv:2010.07763 [cs.PL] https:\/\/arxiv.org\/abs\/2010.07763","journal-title":"Refinement Types: A Tutorial. (2020)"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542510"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_13"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/WCRE.2001.957836"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"J. Gregory Morrisett David Walker Karl Crary and Neal Glew. 1999. From System F to Typed Assembly Language. ACM Transactions on Programming Languages and Systems (TOPLAS) (1999). https:\/\/doi.org\/10.1145\/319301.319345 10.1145\/319301.319345","DOI":"10.1145\/319301.319345"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_1_19_1","author":"Peter David","year":"2023","unstructured":"David Peter. 2023. hyperfine. https:\/\/github.com\/sharkdp\/hyperfine","journal-title":"hyperfine"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485480"},{"key":"e_1_3_1_21_1","author":"Pouchet Louis-Noel","year":"2016","unstructured":"Louis-Noel Pouchet and Tomofumi Yuki. 2016. PolyBench\/C: The Polyhedral benchmark suite, v4.2.1. https:\/\/sourceforge.net\/projects\/polybench\/files\/polybench-c-4.2.1-beta.tar.gz\/download. Accessed: 2023-06-29.","journal-title":"PolyBench\/C: The Polyhedral benchmark suite, v4.2.1"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_59"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706316"},{"key":"e_1_3_1_24_1","author":"Rossberg Andreas","year":"2022","unstructured":"Andreas Rossberg. 2022. WebAssembly Core Specification. https:\/\/www.w3.org\/TR\/wasm-core-2\/ https:\/\/webassembly.github.io\/spec\/core\/_download\/WebAssembly.pdf.","journal-title":"WebAssembly Core Specification"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/231379.231414"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633366"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908110"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507657"},{"key":"e_1_3_1_30_1","author":"Zagieboylo Drew","year":"2020","unstructured":"Drew Zagieboylo, G. Edward Suh, and Andrew C. Myers. 2020. The Cost of Software-Based Memory Management Without Virtual Memory. CoRR abs\/2009.06789 (2020). arXiv:2009.06789 https:\/\/arxiv.org\/abs\/2009.06789","journal-title":"The Cost of Software-Based Memory Management Without Virtual Memory"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00062-5"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632922","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632922","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T18:46:23Z","timestamp":1774982783000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632922"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":30,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632922"],"URL":"https:\/\/doi.org\/10.1145\/3632922","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}