Titill: | A type system with subtyping for WebAssembly’s stack polymorphism |
Höfundur: |
|
Útgáfa: | 2022-10-03 |
Tungumál: | Enska |
Umfang: | 305-323 |
Háskóli/Stofnun: | Reykjavik University Háskólinn í Reykjavík |
Svið: | School of Technology (RU) Tæknisvið (HR) |
Deild: | Department of Computer Science (RU) Tölvunarfræðideild (HR) |
ISBN: | 9783031177149 9783031177156 |
Birtist í: | Lecture Notes in Computer Science;13572 |
ISSN: | 0302-9743 1611-3349 |
DOI: | 10.1007/978-3-031-17715-6_20 |
Efnisorð: | Programming languages (Electronic computers); Semantics; Reasoning; Algorithms; Forritunarmál; Merkingarfræði; Rökfræði; Reiknirit |
URI: | https://hdl.handle.net/20.500.11815/4017 |
Tilvitnun: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
|
|
Útdráttur: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.
|
|
Athugasemdir:Post-print (lokagerð höfundar)
|