{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T19:42:18Z","timestamp":1743018138646,"version":"3.40.3"},"publisher-location":"Cham","reference-count":86,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030891589"},{"type":"electronic","value":"9783030891596"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"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":[[2021]]},"DOI":"10.1007\/978-3-030-89159-6_21","type":"book-chapter","created":{"date-parts":[[2021,10,11]],"date-time":"2021-10-11T17:57:10Z","timestamp":1633975030000},"page":"335-345","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["GATE: Gradual Effect Types"],"prefix":"10.1007","author":[{"given":"Philip","family":"Wadler","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,10,12]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Ahmed, A., Findler, R.B., Siek, J.G., Wadler, P.: Blame for all. In: Principles of Programming Languages (POPL) (2011)","DOI":"10.1145\/1926385.1926409"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Ahmed, A., Jamner, D., Siek, J.G., Wadler, P.: Theorems for free for free: parametricity, with and without types. Proc. ACM Program. Lang. (PACMPL) 1(ICFP), 1\u201328 (2017)","DOI":"10.1145\/3110283"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Atkey, R.: Parameterised notions of computation. In: Mathematically Structured Functional Programming (MSFP). BCS (2006)","DOI":"10.14236\/ewic\/MSFP2006.5"},{"issue":"3\u20134","key":"21_CR4","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1017\/S095679680900728X","volume":"19","author":"R Atkey","year":"2009","unstructured":"Atkey, R.: Parameterised notions of computation. J. Funct. Program. 19(3\u20134), 335\u2013376 (2009)","journal-title":"J. Funct. Program."},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-319-73721-8_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J Bader","year":"2018","unstructured":"Bader, J., Aldrich, J., Tanter, \u00c9.: Gradual program verification. In: VMCAI 2018. LNCS, vol. 10747, pp. 25\u201346. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-73721-8_2"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Schwerter, F.B., Garcia, R., Tanter, \u00c9.: A theory of gradual effect systems. In: International Conference on Functional Programming (ICFP), pp. 283\u2013295. ACM (2014)","DOI":"10.1145\/2692915.2628149"},{"issue":"1","key":"21_CR7","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1016\/j.jlamp.2014.02.001","volume":"84","author":"A Bauer","year":"2015","unstructured":"Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers. J. Logical Algebraic Methods Program. 84(1), 108\u2013123 (2015)","journal-title":"J. Logical Algebraic Methods Program."},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-662-44202-9_11","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"G Bierman","year":"2014","unstructured":"Bierman, G., Abadi, M., Torgersen, M.: Understanding typescript. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 257\u2013281. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44202-9_11"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-14107-2_5","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"G Bierman","year":"2010","unstructured":"Bierman, G., Meijer, E., Torgersen, M.: Adding dynamic types to C$$\\sharp $$. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 76\u2013100. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14107-2_5"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Biernacki, D., Pir\u00f3g, M., Polesiuk, P., Sieczkowski, F.: Binders by day, labels by night: effect instances via lexically scoped handlers. Proc. ACM Program. Lang. (PACMPL) 4(POPL), 48:1\u201348:29 (2020)","DOI":"10.1145\/3371116"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Castagna, G., Lanvin, V., Petrucciani, T., Siek, J.G.: Gradual typing: a new perspective. Proc. ACM Program. Lang. (PACMPL) 3(POPL), 16:1\u201316:32 (2019)","DOI":"10.1145\/3290329"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Chaudhuri, A., Vekris, P., Goldman, S., Roch, M., Levi, G.: Fast and precise type checking for JavaScript. Proc. ACM Program. Lang. (PACMPL) 1(OOPSLA), 48:1\u201348:30 (2017)","DOI":"10.1145\/3133872"},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-73589-2_2","volume-title":"ECOOP 2007 \u2013 Object-Oriented Programming","author":"J Siek","year":"2007","unstructured":"Siek, J., Taha, W.: Gradual typing for objects. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 2\u201327. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73589-2_2"},{"key":"21_CR14","unstructured":"Convent, L., Lindley, S., McBride, C., McLaughlin, C.: Encapsulating effects in Frank (2018)"},{"key":"21_CR15","unstructured":"Courant, N.: Safely typing algebraic effects (2018). http:\/\/gallium.inria.fr\/blog\/safely-typing-algebraic-effects\/"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages (POPL), pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"21_CR17","unstructured":"Dolan, S.: Algebraic Subtyping. BCS, The Chartered Institute for IT (2017)"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Dolan, S., Mycroft, A.: Polymorphism, subtyping, and type inference in MLsub. In: POPL (2017)","DOI":"10.1145\/3009837.3009882"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Eremondi, J., Tanter, \u00c9., Garcia, R.: Approximate normalization for gradual dependent types. Proc. ACM Program. Lang. (PACMPL) 3(ICFP) (2019)","DOI":"10.1145\/3341692"},{"key":"21_CR20","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.scico.2016.06.006","volume":"133","author":"E Ernst","year":"2017","unstructured":"Ernst, E., M\u00f8ller, A., Schwarz, M., Strocco, F.: Message safety in dart. Sci. Comput. Program. 133, 51\u201373 (2017)","journal-title":"Sci. Comput. Program."},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Filinski, A.: Representing monads. In: Principles of Programming Languages (POPL), pp. 446\u2013457. ACM (1994)","DOI":"10.1145\/174675.178047"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Filinski, A.: Representing layered monads. In: Principles of Programming Languages (POPL), pp. 175\u2013188. ACM (1999)","DOI":"10.1145\/292540.292557"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Findler, R.B., Felleisen, M.: Contracts for higher-order functions. In: International Conference on Functional Programming (ICFP), pp. 48\u201359. ACM, October 2002","DOI":"10.1145\/583852.581484"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Flanagan, C.: Hybrid type checking. In: Principles of Programming Languages (POPL), pp. 245\u2013256. ACM, January 2006","DOI":"10.1145\/1111320.1111059"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Forster, Y., Kammar, O., Lindley, S., Pretnar, M.: On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control. Proc. ACM Program. Lang. (PACMPL) 1(ICFP), 13:1\u201313:29 (2017)","DOI":"10.1145\/3110257"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"Garcia, R.: Calculating threesomes, with blame. In: International Conference on Functional Programming (ICFP) (2013)","DOI":"10.1145\/2500365.2500603"},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"Garcia, R., Clark, A.M., Tanter, \u00c9.: Abstracting gradual typing. In: Principles of Programming Languages (POPL), pp. 429\u2013442. ACM (2016)","DOI":"10.1145\/2914770.2837670"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Gifford, D.K., Lucassen, J.M.: Integrating functional and imperative programming. In: LISP and Functional Programming, pp. 28\u201338. ACM (1986)","DOI":"10.1145\/319838.319848"},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"Greenman, B., Felleisen, M.: A spectrum of type soundness and performance. Proc. ACM Program. Lang. (PACMPL) 2(ICFP), 71:1\u201371:32 (2018)","DOI":"10.1145\/3236766"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"Guha, A., Matthews, J., Findler, R.B., Krishnamurthi, S.: Relationally-parametric polymorphic contracts. In: Dynamic Languages Symposium (DLS), pp. 29\u201340 (2007)","DOI":"10.1145\/1297081.1297089"},{"key":"21_CR31","unstructured":"Herman, D., Tomb, A., Flanagan, C.: Space-efficient gradual typing. In: Trends in Functional Programming (TFP) (2007)"},{"key":"21_CR32","doi-asserted-by":"crossref","unstructured":"Hillerstr\u00f6m, D., Lindley, S.: Liberating effects with rows and handlers. In: Proceedings of the 1st International Workshop on Type-Driven Development, pp. 15\u201327. ACM (2016)","DOI":"10.1145\/2976022.2976033"},{"key":"21_CR33","unstructured":"Hillerstr\u00f6m, D., Lindley, S., Atkey, R., Sivaramakrishnan, K.C.: Continuation passing style for effect handlers. In: Formal Structures for Computation and Deduction (FSCD), vol. 84. LIPIcs, pp. 18:1\u201319. Schloss Dagstuhl (2017)"},{"key":"21_CR34","doi-asserted-by":"crossref","unstructured":"Igarashi, A., Thiemann, P., Vasconcelos, V.T., Wadler, P.: Gradual session types. Proc. ACM Program. Lang. (PACMPL) 1(ICFP), 38 (2017)","DOI":"10.1145\/3110282"},{"key":"21_CR35","doi-asserted-by":"crossref","unstructured":"Kammar, O., Plotkin, G.D.: Algebraic foundations for effect-dependent optimisations. In: Principles of Programming Languages (POPL), pp. 349\u2013360. ACM (2012)","DOI":"10.1145\/2103621.2103698"},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"Katsumata, S.-Y.: Parametric effect monads and semantics of effect systems. In: Principles of Programming Languages (POPL), pp. 633\u2013646. ACM (2014)","DOI":"10.1145\/2535838.2535846"},{"key":"21_CR37","doi-asserted-by":"publisher","unstructured":"King, D.J., Wadler, P.: Combining monads. In: Launchbury, J., Sansom, P. (eds.) Glasgow Workshop on Functional Programming, Workshops in Computing, pp. 134\u2013143. Springer, London (1992). https:\/\/doi.org\/10.1007\/978-1-4471-3215-8_12","DOI":"10.1007\/978-1-4471-3215-8_12"},{"key":"21_CR38","doi-asserted-by":"crossref","unstructured":"Leijen, D.: Type directed compilation of row-typed algebraic effects. In: Principles of Programming Languages (POPL), pp. 486\u2013499. ACM, January 2017","DOI":"10.1145\/3093333.3009872"},{"key":"21_CR39","doi-asserted-by":"crossref","unstructured":"Liang, S., Hudak, P., Jones, M.P.: Monad transformers and modular interpreters. In: Principles of Programming Languages (POPL), pp. 333\u2013343. ACM (1995)","DOI":"10.1145\/199448.199528"},{"key":"21_CR40","doi-asserted-by":"crossref","unstructured":"Lindley, S., McBride, C., McLaughlin, C.: Do be do be do. In: Principles of Programming Languages (POPL), pp. 500\u2013514. ACM, January 2017","DOI":"10.1145\/3093333.3009897"},{"key":"21_CR41","doi-asserted-by":"crossref","unstructured":"Marino, D., Millstein, T.: A generic type-and-effect system. In: Types in Language Design and Implementation (TLDI), pp. 39\u201350. ACM (2009)","DOI":"10.1145\/1481861.1481868"},{"key":"21_CR42","doi-asserted-by":"crossref","unstructured":"Matthews, J., Findler, R.B.: Operational semantics for multi-language programs. In: Principles of Programming Languages (POPL), pp. 3\u201310 (2007)","DOI":"10.1145\/1190215.1190220"},{"key":"21_CR43","unstructured":"McBride, C.: Shonky (2016). https:\/\/github.com\/pigworker\/shonky"},{"issue":"3","key":"21_CR44","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R Milner","year":"1978","unstructured":"Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17(3), 348\u2013375 (1978)","journal-title":"J. Comput. Syst. Sci."},{"key":"21_CR45","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C.: Coercion and type inference. In: Principles of Programming Languages (POPL), pp. 175\u2013185. ACM (1984)","DOI":"10.1145\/800017.800529"},{"key":"21_CR46","unstructured":"Moggi, E.: Computational lambda-calculus and monads. In: Symposium on Logic in Computer Science (LICS), pp. 14\u201323. IEEE (1989)"},{"issue":"1","key":"21_CR47","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55\u201392 (1991)","journal-title":"Inf. Comput."},{"key":"21_CR48","doi-asserted-by":"crossref","unstructured":"Garrett Morris, J., McKinna, J.: Abstracting extensible data types: or, rows by any other name. Proc. ACM Program. Lang. (PACMPL) 3(POPL), 12 (2019)","DOI":"10.1145\/3290325"},{"key":"21_CR49","doi-asserted-by":"crossref","unstructured":"New, M.S., Licata, D.R., Ahmed, A.: Gradual type theory. Proc. ACM Program. Lang. (PACMPL) 3(POPL), 15:1\u201315:31 (2019)","DOI":"10.1145\/3290328"},{"key":"21_CR50","doi-asserted-by":"crossref","unstructured":"New, M.S., Jamner, D., Ahmed, A.: Graduality and parametricity: together again for the first time. Proc. ACM Program. Lang. (PACMPL) 4(POPL), 1\u201332 (2020)","DOI":"10.1145\/3371114"},{"key":"21_CR51","doi-asserted-by":"crossref","unstructured":"Orchard, D., Wadler, P., Eades III, H.: Unifying graded and parameterised monads. In: Mathematically Structured Functional Programming (MSFP), vol. 317. EPTCS, pp. 18\u201338 (2020)","DOI":"10.4204\/EPTCS.317.2"},{"key":"21_CR52","unstructured":"Orchard, D.A., Petricek, T., Mycroft, A.: The semantic marriage of monads and effects. CoRR, abs\/1401.5391 (2014). http:\/\/arxiv.org\/abs\/1401.5391"},{"key":"21_CR53","series-title":"IFIP International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/1-4020-8141-3_34","volume-title":"Exploring New Frontiers of Theoretical Informatics","author":"X Ou","year":"2004","unstructured":"Ou, X., Tan, G., Mandelbaum, Y., Walker, D.: Dynamic typing with dependent types. In: Levy, J.-J., Mayr, E.W., Mitchell, J.C. (eds.) TCS 2004. IIFIP, vol. 155, pp. 437\u2013450. Springer, Boston, MA (2004). https:\/\/doi.org\/10.1007\/1-4020-8141-3_34"},{"key":"21_CR54","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1016\/S1571-0661(04)80970-8","volume":"45","author":"G Plotkin","year":"2001","unstructured":"Plotkin, G., Power, J.: Semantics for algebraic operations. Electron. Notes Theoret. Comput. Sci. (ENTCS) 45, 332\u2013345 (2001a)","journal-title":"Electron. Notes Theoret. Comput. Sci. (ENTCS)"},{"key":"21_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45315-6_1","volume-title":"Foundations of Software Science and Computation Structures","author":"G Plotkin","year":"2001","unstructured":"Plotkin, G., Power, J.: Adequacy for algebraic effects. In: Honsell, F., Miculan, M. (eds.) FoSSaCS 2001. LNCS, vol. 2030, pp. 1\u201324. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45315-6_1"},{"key":"21_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-00590-9_7","volume-title":"Programming Languages and Systems","author":"G Plotkin","year":"2009","unstructured":"Plotkin, G., Pretnar, M.: Handlers of algebraic effects. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 80\u201394. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00590-9_7"},{"key":"21_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-45931-6_24","volume-title":"Foundations of Software Science and Computation Structures","author":"G Plotkin","year":"2002","unstructured":"Plotkin, G., Power, J.: Notions of computation determine monads. In: Nielsen, M., Engberg, U. (eds.) FoSSaCS 2002. LNCS, vol. 2303, pp. 342\u2013356. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45931-6_24"},{"issue":"1","key":"21_CR58","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1023\/A:1023064908962","volume":"11","author":"GD Plotkin","year":"2003","unstructured":"Plotkin, G.D., Power, J.: Algebraic operations and generic effects. Appl. Categ. Struct. 11(1), 69\u201394 (2003)","journal-title":"Appl. Categ. Struct."},{"key":"21_CR59","doi-asserted-by":"crossref","unstructured":"Plotkin, G.D., Pretnar, M.: A logic for algebraic effects. In: Symposium on Logic in Computer Science (LICS), pp. 118\u2013129. IEEE (2008)","DOI":"10.1109\/LICS.2008.45"},{"key":"21_CR60","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP congress, vol. 83 (1983)"},{"key":"21_CR61","doi-asserted-by":"crossref","unstructured":"Schwerter, F.B., Garcia, R., Tanter, \u00c9.: Gradual type-and-effect systems. J. Funct. Program. 26 (2016)","DOI":"10.1017\/S0956796816000162"},{"key":"21_CR62","doi-asserted-by":"crossref","unstructured":"Siek, J., Thiemann, P., Wadler, P.: Blame and coercion: together again for the first time. In: Programming Language Design and Implementation (PLDI) (2015a)","DOI":"10.1145\/2737924.2737968"},{"key":"21_CR63","unstructured":"Jeremy G. Siek and Walid Taha. Gradual typing for functional languages. In: Scheme and Functional Programming Workshop (Scheme), pp. 81\u201392, September 2006"},{"key":"21_CR64","doi-asserted-by":"crossref","unstructured":"Siek, J.G., Wadler, P.: Threesomes, with and without blame. In: Principles of Programming Languages (POPL) (2010)","DOI":"10.1145\/1706299.1706342"},{"key":"21_CR65","unstructured":"Siek, J.G., Vitousek, M.M., Cimini, M., Boyland, J.T.: Refined criteria for gradual typing. In: Summit on Advances in Programming Languages (SNAPL), vol. 32. LIPIcs, pp. 274\u2013293. Schloss Dagstuhl (2015b)"},{"issue":"2","key":"21_CR66","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1006\/inco.1994.1046","volume":"111","author":"J-P Talpin","year":"1994","unstructured":"Talpin, J.-P., Jouvelot, P.: The type and effect discipline. Inf. Comput. 111(2), 245\u2013296 (1994)","journal-title":"Inf. Comput."},{"key":"21_CR67","doi-asserted-by":"crossref","unstructured":"Tobin-Hochstadt, S., Felleisen, M.: Interlanguage migration: from scripts to programs. In: Object-Oriented Programming: Systems, Languages, and Applications (OOPSLA), pp. 964\u2013974. ACM (2006)","DOI":"10.1145\/1176617.1176755"},{"key":"21_CR68","doi-asserted-by":"crossref","unstructured":"Tobin-Hochstadt, S., Felleisen, M.: The design and implementation of typed scheme. In: Principles of Programming Languages (POPL), pp. 395\u2013406. ACM (2008)","DOI":"10.1145\/1328897.1328486"},{"key":"21_CR69","doi-asserted-by":"crossref","unstructured":"Toro, M., Garcia, R., Tanter, \u00c9.: Type-driven gradual security with references. ACM Trans. Program. Lang. Syst. 40(4), 1\u201355 2018","DOI":"10.1145\/3229061"},{"key":"21_CR70","doi-asserted-by":"crossref","unstructured":"Toro, M., Labrada, E., Tanter, \u00c9.: Gradual parametricity, revisited. Proc. ACM Program. Lang. (PACMPL) 3(POPL) (2019)","DOI":"10.1145\/3290330"},{"key":"21_CR71","unstructured":"Verlaguet, J.: Facebook: analysing PHP statically. In: Workshop on Commercial Uses of Functional Programming (CUFP) (2013)"},{"key":"21_CR72","doi-asserted-by":"crossref","unstructured":"Vitousek, M.M., Swords, C., Siek, J.G.: Big types in little runtime: open-world soundness and collaborative blame for gradual type systems. In: Principles of Programming Languages (POPL), pp. 762\u2013774. ACM (2017)","DOI":"10.1145\/3093333.3009849"},{"key":"21_CR73","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Theorems for free! In: Functional Programming Languages and Computer Architecture (FPCA) (1989)","DOI":"10.1145\/99370.99404"},{"key":"21_CR74","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Comprehending monads. In: LISP and Functional Programming, pp. 61\u201378. ACM (1990)","DOI":"10.1145\/91556.91592"},{"key":"21_CR75","doi-asserted-by":"crossref","unstructured":"Wadler, P.: The essence of functional programming. In: Principles of Programming Languages (POPL), pp. 1\u201314. ACM (1992)","DOI":"10.1145\/143165.143169"},{"issue":"1","key":"21_CR76","first-page":"39","volume":"7","author":"P Wadler","year":"1994","unstructured":"Wadler, P.: Monads and composable continuations. LISP Symb. Comput. 7(1), 39\u201356 (1994)","journal-title":"LISP Symb. Comput."},{"key":"21_CR77","doi-asserted-by":"crossref","unstructured":"Wadler, P.: The marriage of effects and monads. In: International Conference on Functional Programming (ICFP), pp. 63\u201374. ACM (1998)","DOI":"10.1145\/291251.289429"},{"key":"21_CR78","unstructured":"Wadler, P.: A complement to blame. In: Summit on Advances in Programming Languages (SNAPL), vol. 32. LIPIcs, pp. 309\u2013320. Schloss Dagstuhl (2015)"},{"key":"21_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-00590-9_1","volume-title":"Programming Languages and Systems","author":"P Wadler","year":"2009","unstructured":"Wadler, P., Findler, R.B.: Well-typed programs can\u2019t be blamed. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 1\u201316. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00590-9_1"},{"issue":"1","key":"21_CR80","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/601775.601776","volume":"4","author":"P Wadler","year":"2003","unstructured":"Wadler, P., Thiemann, P.: The marriage of effects and monads. Trans. Comput. Logic (TOCL) 4(1), 1\u201332 (2003)","journal-title":"Trans. Comput. Logic (TOCL)"},{"key":"21_CR81","doi-asserted-by":"crossref","unstructured":"Wand, M.: Type inference for record concatenation and multiple inheritance. In: Symposium on Logic in Computer Science (LICS), pp. 92\u201397. IEEE (1989)","DOI":"10.1109\/LICS.1989.39162"},{"issue":"1","key":"21_CR82","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90050-C","volume":"93","author":"M Wand","year":"1991","unstructured":"Wand, M.: Type inference for record concatenation and multiple inheritance. Inf. Comput. 93(1), 1\u201315 (1991)","journal-title":"Inf. Comput."},{"key":"21_CR83","doi-asserted-by":"crossref","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38\u201394 (1994)","DOI":"10.1006\/inco.1994.1093"},{"key":"21_CR84","unstructured":"Zalewski, J., Mckinna, J., Garrett Morris, J., Wadler, P.: $$\\lambda $$db: blame tracking at higher fidelity. In: Workshop on Gradual Typing (2020)"},{"key":"21_CR85","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Myers, A.C.: Abstraction-safe effect handlers via tunneling. Proc. ACM Program. Lang. (PACMPL) 3(POPL), 5 (2019)","DOI":"10.1145\/3290318"},{"key":"21_CR86","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Salvaneschi, G., Beightol, Q., Liskov, B., Myers, A.C.: Accepting blame for safe tunneled exceptions. In: Programming Language Design and Implementation (PLDI), pp. 281\u2013295. ACM (2016)","DOI":"10.1145\/2980983.2908086"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-89159-6_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T20:26:47Z","timestamp":1725913607000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-89159-6_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030891589","9783030891596"],"references-count":86,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-89159-6_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"12 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 October 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 October 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/isola-conference.org\/isola2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}