dc.contributor |
Reykjavik University |
dc.contributor |
Háskólinn í Reykjavík |
dc.contributor.author |
McDermott, Dylan |
dc.contributor.author |
Morita, Yasuaki |
dc.contributor.author |
Uustalu, Tarmo |
dc.date.accessioned |
2023-02-21T13:57:37Z |
dc.date.available |
2023-02-21T13:57:37Z |
dc.date.issued |
2022-10-03 |
dc.identifier.citation |
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 |
dc.identifier.isbn |
9783031177149 |
dc.identifier.isbn |
9783031177156 |
dc.identifier.issn |
0302-9743 |
dc.identifier.issn |
1611-3349 |
dc.identifier.uri |
https://hdl.handle.net/20.500.11815/4017 |
dc.description |
Post-print (lokagerð höfundar) |
dc.description.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. |
dc.description.sponsorship |
This work was supported by the Icelandic Research Fund grant no. 196323-053. |
dc.format.extent |
305-323 |
dc.language.iso |
en |
dc.publisher |
Springer |
dc.relation.ispartofseries |
Lecture Notes in Computer Science;13572 |
dc.rights |
info:eu-repo/semantics/embargoedAccess |
dc.subject |
Programming languages (Electronic computers) |
dc.subject |
Semantics |
dc.subject |
Reasoning |
dc.subject |
Algorithms |
dc.subject |
Forritunarmál |
dc.subject |
Merkingarfræði |
dc.subject |
Rökfræði |
dc.subject |
Reiknirit |
dc.title |
A type system with subtyping for WebAssembly’s stack polymorphism |
dc.type |
info:eu-repo/semantics/bookPart |
dc.description.version |
Peer reviewed (ritrýnd grein) |
dc.identifier.journal |
Theoretical Aspects of Computing – ICTAC 2022: 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings |
dc.identifier.doi |
10.1007/978-3-031-17715-6_20 |
dc.relation.url |
https://link.springer.com/content/pdf/10.1007/978-3-031-17715-6_20 |
dc.contributor.department |
Department of Computer Science (RU) |
dc.contributor.department |
Tölvunarfræðideild (HR) |
dc.contributor.school |
School of Technology (RU) |
dc.contributor.school |
Tæknisvið (HR) |