Opin vísindi

A type system with subtyping for WebAssembly’s stack polymorphism

A type system with subtyping for WebAssembly’s stack polymorphism

Title: A type system with subtyping for WebAssembly’s stack polymorphism
Author: McDermott, Dylan   orcid.org/0000-0002-6705-1449
Morita, Yasuaki   orcid.org/0000-0002-8005-2454
Uustalu, Tarmo   orcid.org/0000-0002-1297-0579
Date: 2022-10-03
Language: English
Scope: 305-323
University/Institute: Reykjavik University
Háskólinn í Reykjavík
School: School of Technology (RU)
Tæknisvið (HR)
Department: Department of Computer Science (RU)
Tölvunarfræðideild (HR)
ISBN: 9783031177149
Series: Lecture Notes in Computer Science;13572
ISSN: 0302-9743
DOI: 10.1007/978-3-031-17715-6_20
Subject: Programming languages (Electronic computers); Semantics; Reasoning; Algorithms; Forritunarmál; Merkingarfræði; Rökfræði; Reiknirit
URI: https://hdl.handle.net/20.500.11815/4017

Show full item record


D. McDermott, Y. Morita, T. Uustalu. A type system with subtyping for WebAssembly's stack polymorphism. In H. Seidl, Z. Liu, C. S. Pasareanu, eds., Theoretical Aspects of Computing – ICTAC 2022: 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings, Lecture Notes in Computer Science, v. 13572, pp. 305-323. Springer, Cham, 2022. doi:10.1007/978-3-031-17715-6_20


We propose a new type system for WebAssembly. It is a refinement of the type system from the language specification and is based on type qualifiers and subtyping. In the WebAssembly specification, a typable instruction sequence gets many different types, depending in particular on whether it contains instructions such as br (unconditional branch) that are stack-polymorphic in an unusual way. But one cannot single out a canonical type for a typable instruction sequence satisfactorily. We introduce qualifiers on code types to distinguish between the two flavors of stack polymorphism that occur in WebAssembly and a subtyping relation on such qualified types. Our type system gives every typable instruction sequence a canonical type that is principal. We show that the new type system is in a precise relationship to the type system given in the WebAssembly specification. In addition, we describe a typed functional-style big-step semantics based on this new type system underpinned by an indexed graded monad and prove that it prevents stack-manipulation related runtime errors. We have formalized our type system, inference algorithm, and semantics in Agda.


Post-print (lokagerð höfundar)

Files in this item

This item appears in the following Collection(s)