A type system with subtyping for WebAssembly’s stack polymorphism

Dylan McDermott, Yasuaki Morita, Tarmo Uustalu

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.
Original languageEnglish
Title of host publicationTheoretical Aspects of Computing – ICTAC 2022
Subtitle of host publication19th International Colloquium, Tbilisi, Georgia, September 27–29, 2022, Proceedings
EditorsHelmut Seidl, Zhiming Liu, Corina S. Pasareanu
PublisherSpringer, Cham
Pages305-323
ISBN (Electronic)978-3-031-17715-6
ISBN (Print)978-3-031-17714-9
DOIs
Publication statusPublished - 3 Oct 2022
Event19th International Colloquium on Theoretical Aspects of Computing - Tbilisi, Georgia
Duration: 27 Sept 202230 Sept 2022
https://viam.science.tsu.ge/clas2022/ictac/

Publication series

NameLecture Notes in Computer Science
Volume13572
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference19th International Colloquium on Theoretical Aspects of Computing
Abbreviated titleICTAC 2022
Country/TerritoryGeorgia
CityTbilisi
Period27/09/2230/09/22
Internet address

Bibliographical note

Funding Information:
This work was supported by the Icelandic Research Fund grant no. 196323-053.

Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Fingerprint

Dive into the research topics of 'A type system with subtyping for WebAssembly’s stack polymorphism'. Together they form a unique fingerprint.

Cite this