{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T08:43:48Z","timestamp":1743151428440,"version":"3.40.3"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031177149"},{"type":"electronic","value":"9783031177156"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-17715-6_20","type":"book-chapter","created":{"date-parts":[[2022,10,2]],"date-time":"2022-10-02T09:02:27Z","timestamp":1664701347000},"page":"305-323","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Type System with\u00a0Subtyping for\u00a0WebAssembly\u2019s Stack Polymorphism"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6705-1449","authenticated-orcid":false,"given":"Dylan","family":"McDermott","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8005-2454","authenticated-orcid":false,"given":"Yasuaki","family":"Morita","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1297-0579","authenticated-orcid":false,"given":"Tarmo","family":"Uustalu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,10,3]]},"reference":[{"issue":"1","key":"20_CR1","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1017\/s0960129517000184","volume":"29","author":"J Chapman","year":"2019","unstructured":"Chapman, J., Uustalu, T., Veltri, N.: Quotienting the delay monad by weak bisimilarity. Math. Struct. Comput. Sci. 29(1), 67\u201392 (2019). https:\/\/doi.org\/10.1017\/s0960129517000184","journal-title":"Math. Struct. Comput. Sci."},{"key":"20_CR2","doi-asserted-by":"publisher","unstructured":"Haas, A., Rossberg, A., Schuff, D.L., Titzer, B.L., Holman, M., Gohman, D., Wagner, L., Zakai, A., Bastien, J.F.: Bringing the Web up to speed with WebAssembly. In: Proc. of 38th ACM SIGPLAN Conf. on Programming Language Design and Implementation, PLDI 2017, pp. 185\u2013200. ACM Press, New York (2017). https:\/\/doi.org\/10.1145\/3062341.3062363","DOI":"10.1145\/3062341.3062363"},{"key":"20_CR3","unstructured":"Huang, X.: A Mechanized Formalization of the WebAssembly Specification in Coq. Master\u2019s thesis, Rochester Institute of Technology (2019). https:\/\/www.cs.rit.edu\/~mtf\/student-resources\/20191_huang_mscourse.pdf"},{"key":"20_CR4","doi-asserted-by":"publisher","unstructured":"Katsumata, S.: Parametric effect monads and semantics of effect systems. In: Proceedings of 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 633\u2013645. ACM Press, New York (2014). https:\/\/doi.org\/10.1145\/2535838.2535846","DOI":"10.1145\/2535838.2535846"},{"key":"20_CR5","unstructured":"Melli\u00e8s, P.A.: Parametric monads and enriched adjunctions. Manuscript (2012). https:\/\/www.irif.fr\/~mellies\/tensorial-logic\/8-parametric-monads-and-enriched-adjunctions.pdf"},{"issue":"5","key":"20_CR6","doi-asserted-by":"publisher","first-page":"957","DOI":"10.1017\/s0956796801004178","volume":"13","author":"G Morrisett","year":"2003","unstructured":"Morrisett, G., Crary, K., Glew, N., Walker, D.: Stack-based typed assembly language. J. Funct. Program. 13(5), 957\u2013959 (2003). https:\/\/doi.org\/10.1017\/s0956796801004178","journal-title":"J. Funct. Program."},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-642-03359-9_26","volume-title":"Theorem Proving in Higher Order Logics","author":"K Nakata","year":"2009","unstructured":"Nakata, K., Uustalu, T.: Trace-based coinductive operational semantics for While. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 375\u2013390. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_26"},{"key":"20_CR8","unstructured":"Nivat, M., Perrot, J.F.: Une g\u00e9n\u00e9ralisation du mono\u00efde bicyclique. Comptes Rendus Acad. Sci. Paris, Ser. A 271, 824\u2013827 (1970). https:\/\/gallica.bnf.fr\/ark:\/12148\/bpt6k480299v\/f830"},{"key":"20_CR9","unstructured":"P\u00f6ial, J.: Algebraic specification of stack-effects for Forth-programs. In: 1990 FORML Conference Proceedings, pp. 282\u2013290. Forth Interest Group (1991). https:\/\/www.kodu.ee\/~jpoial\/teadus\/EuroForth90_Algebraic.pdf"},{"key":"20_CR10","unstructured":"Rossberg, A.: WebAssembly core specification, version 1.1. Editor\u2019s Draft, 18 Dec. 2021 (2021). https:\/\/webassembly.github.io\/spec\/core\/"},{"issue":"3","key":"20_CR11","doi-asserted-by":"publisher","first-page":"3032","DOI":"10.1007\/s10958-008-9013-7","volume":"151","author":"A Smirnov","year":"2008","unstructured":"Smirnov, A.: Graded monads and rings of polynomials. J. Math. Sci. 151(3), 3032\u20133051 (2008). https:\/\/doi.org\/10.1007\/s10958-008-9013-7","journal-title":"J. Math. Sci."},{"key":"20_CR12","doi-asserted-by":"publisher","unstructured":"Sti\u00e9venart, Q., De Roover, C.: Compositional information flow analysis for WebAssembly programs. In: Proceedings of IEEE 20th International Working Conference on Source Code Analysis and Manipulation, SCAM 2020, pp. 13\u201324. IEEE, Los Alamitos (2020). https:\/\/doi.org\/10.1109\/scam51674.2020.00007","DOI":"10.1109\/scam51674.2020.00007"},{"issue":"4","key":"20_CR13","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/bf01212404","volume":"5","author":"B Stoddart","year":"1993","unstructured":"Stoddart, B., Knaggs, P.J.: Type inference in stack based languages. Formal Aspects Comput. 5(4), 289\u2013298 (1993). https:\/\/doi.org\/10.1007\/bf01212404","journal-title":"Formal Aspects Comput."},{"key":"20_CR14","unstructured":"W3C: WebAssembly core specification, version 1.0. W3C Recommendation, 5 Dec. 2019 (2019). https:\/\/www.w3.org\/TR\/wasm-core-1"},{"key":"20_CR15","doi-asserted-by":"publisher","unstructured":"Watt, C.: Mechanising and verifying the WebAssembly specification. In: Proceedings of 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pp. 53\u201365. ACM Press, New York (2018). https:\/\/doi.org\/10.1145\/3167082","DOI":"10.1145\/3167082"},{"key":"20_CR16","doi-asserted-by":"publisher","unstructured":"Watt, C., Maksimovic, P., Krishnaswami, N.R., Gardner, P.: A program logic for first-order encapsulated WebAssembly. In: Donaldson, A.F. (ed.) Proceedings of 33rd European Conference on Object-Oriented Programming, ECOOP 2019, Leibniz International Proceedings in Information, vol. 134, pp. 9:1\u20139:30. Dagstuhl Publishing, Saarbr\u00fccken\/Wadern (2019). https:\/\/doi.org\/10.4230\/lipics.ecoop.2019.9","DOI":"10.4230\/lipics.ecoop.2019.9"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-030-90870-6_4","volume-title":"Formal Methods","author":"C Watt","year":"2021","unstructured":"Watt, C., Rao, X., Pichon-Pharabod, J., Bodin, M., Gardner, P.: Two mechanisations of webassembly 1.0. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 61\u201379. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_4"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2022"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-17715-6_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,2]],"date-time":"2022-10-02T23:04:21Z","timestamp":1664751861000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-17715-6_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031177149","9783031177156"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-17715-6_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"3 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tbilisi","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Georgia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 September 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/viam.science.tsu.ge\/clas2022\/ictac\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}