A Type System with Subtyping for WebAssembly's Stack Polymorphism

Yasuaki Morita

Reykjavik University



Abstract: We propose a new type system with subtyping relation and qualifiers over shapes of operand stack for WebAssembly. Our type system has two kinds of qualifiers, and we show that the type inference algorithm gives principal types even for codes with stack polymorphic properties. We show that the new type system has a precise relationship to the type system given in the WebAssembly specification. In addition, we give a denotational semantics based on the new type system.