{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T05:57:28Z","timestamp":1777874248999,"version":"3.51.4"},"publisher-location":"Cham","reference-count":61,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227195","type":"print"},{"value":"9783032227201","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"},{"start":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T00:00:00Z","timestamp":1775779200000},"content-version":"vor","delay-in-days":99,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22720-1_15","type":"book-chapter","created":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T15:30:12Z","timestamp":1775748612000},"page":"401-431","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Category-Theoretic Framework for Dependent Effect Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3954-8255","authenticated-orcid":false,"given":"Satoshi","family":"Kura","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5235-7066","authenticated-orcid":false,"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9286-230X","authenticated-orcid":false,"given":"Taro","family":"Sekiyama","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4225-8195","authenticated-orcid":false,"given":"Hiroshi","family":"Unno","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,10]]},"reference":[{"issue":"OOPSLA2","key":"15_CR1","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1145\/3563313","volume":"6","author":"C Abuah","year":"2022","unstructured":"Abuah, C., Darais, D., Near, J.P.: Solo: a lightweight static analysis for differential privacy. Proc. ACM Program. Lang. 6(OOPSLA2), 699\u2013728 (2022). https:\/\/doi.org\/10.1145\/3563313","journal-title":"Proc. ACM Program. Lang."},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Katsumata, S.y., Sato, T.: Higher-order probabilistic adversarial computations: Categorical semantics and program logics. Proceedings of the ACM on Programming Languages 5(ICFP), 1\u201330 (Aug 2021)","DOI":"10.1145\/3473598"},{"key":"15_CR3","unstructured":"Ahman, D.: Fibred Computational Effects. Ph.D. thesis, University of Edinburgh (2017)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Ahman, D., Ghani, N., Plotkin, G.D.: Dependent Types and Fibred Computational Effects. In: Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science, vol.\u00a09634, pp. 36\u201354. Springer Berlin Heidelberg, Berlin, Heidelberg (2016)","DOI":"10.1007\/978-3-662-49630-5_3"},{"key":"15_CR5","doi-asserted-by":"publisher","unstructured":"Atkey, R.: Parameterised notions of computation. J. Funct. Program. 19(3\u20134), 335\u2013376 (Jul 2009). https:\/\/doi.org\/10.1017\/S095679680900728X","DOI":"10.1017\/S095679680900728X"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: Cvc5: A Versatile and Industrial-Strength SMT Solver. In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 13243, pp. 415\u2013442. Springer International Publishing, Cham (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gaboardi, M., Gallego\u00a0Arias, E.J., Hsu, J., Roth, A., Strub, P.Y.: Higher-order approximate relational refinement types for mechanism design and differential privacy. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL \u201915. pp. 55\u201368. ACM Press, Mumbai, India (2015)","DOI":"10.1145\/2676726.2677000"},{"key":"15_CR8","unstructured":"Barthe, G., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.Y.: A program logic for union bounds. In: 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (Lipics), vol.\u00a055, pp. 107:1\u2013107:15. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2016)"},{"key":"15_CR9","doi-asserted-by":"publisher","unstructured":"Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, USA, 23-25 June 2008. pp. 17\u201332. IEEE Computer Society (2008). https:\/\/doi.org\/10.1109\/CSF.2008.27","DOI":"10.1109\/CSF.2008.27"},{"key":"15_CR10","doi-asserted-by":"publisher","unstructured":"Breuvart, F., McDermott, D., Uustalu, T.: Canonical gradings of monads. In: Master, J., Lewis, M. (eds.) Proceedings Fifth International Conference on Applied Category Theory, ACT 2022, Glasgow, United Kingdom, 18-22 July 2022. EPTCS, vol.\u00a0380, pp. 1\u201321 (2022). https:\/\/doi.org\/10.4204\/EPTCS.380.1","DOI":"10.4204\/EPTCS.380.1"},{"key":"15_CR11","doi-asserted-by":"publisher","unstructured":"\u00c7i\u00e7ek, E., Barthe, G., Gaboardi, M., Garg, D., Hoffmann, J.: Relational cost analysis. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 316\u2013329. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009858","DOI":"10.1145\/3009837.3009858"},{"key":"15_CR12","doi-asserted-by":"publisher","unstructured":"\u00c7i\u00e7ek, E., Garg, D., Acar, U.A.: Refinement types for incremental computational complexity. In: Vitek, J. (ed.) Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. Lecture Notes in Computer Science, vol.\u00a09032, pp. 406\u2013431. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_17","DOI":"10.1007\/978-3-662-46669-8_17"},{"key":"15_CR13","doi-asserted-by":"publisher","unstructured":"Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely functional data structures. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 133\u2013144. POPL \u201908, Association for Computing Machinery, New York, NY, USA (2008). https:\/\/doi.org\/10.1145\/1328438.1328457","DOI":"10.1145\/1328438.1328457"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol.\u00a04963, pp. 337\u2013340. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: Computer Aided Verification. Lecture Notes in Computer Science, vol.\u00a08559, pp. 737\u2013744. Springer International Publishing, Cham (2014)","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"15_CR16","doi-asserted-by":"publisher","unstructured":"Fujii, S., Katsumata, S., Melli\u00e8s, P.: Towards a formal theory of graded monads. In: Jacobs, B., L\u00f6ding, C. (eds.) Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09634, pp. 513\u2013530. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49630-5_30","DOI":"10.1007\/978-3-662-49630-5_30"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Gaboardi, M., Katsumata, S.y., Orchard, D., Sato, T.: Graded Hoare Logic and its Categorical Semantics. In: Programming Languages and Systems. Lecture Notes in Computer Science, vol. 12648, pp. 234\u2013263. Springer International Publishing, Cham (2021)","DOI":"10.1007\/978-3-030-72019-3_9"},{"key":"15_CR18","doi-asserted-by":"publisher","unstructured":"Gaboardi, M., Katsumata, S., Orchard, D.A., Breuvart, F., Uustalu, T.: Combining effects and coeffects via grading. In: Garrigue, J., Keller, G., Sumii, E. (eds.) Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016. pp. 476\u2013489. ACM (2016). https:\/\/doi.org\/10.1145\/2951913.2951939","DOI":"10.1145\/2951913.2951939"},{"key":"15_CR19","doi-asserted-by":"publisher","unstructured":"Gordon, C.S.: Polymorphic iterable sequential effect systems. ACM Trans. Program. Lang. Syst. 43(1), 4:1\u20134:79 (2021). https:\/\/doi.org\/10.1145\/3450272","DOI":"10.1145\/3450272"},{"key":"15_CR20","doi-asserted-by":"publisher","unstructured":"Grobauer, B.: Cost recurrences for dml programs. In: Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming. p. 253\u2013264. ICFP \u201901, Association for Computing Machinery, New York, NY, USA (2001). https:\/\/doi.org\/10.1145\/507635.507666","DOI":"10.1145\/507635.507666"},{"key":"15_CR21","doi-asserted-by":"publisher","unstructured":"Grodin, H., Niu, Y., Sterling, J., Harper, R.: Decalf: A directed, effectful cost-aware logical framework. Proc. ACM Program. Lang. 8(POPL), 273\u2013301 (2024). https:\/\/doi.org\/10.1145\/3632852","DOI":"10.1145\/3632852"},{"key":"15_CR22","doi-asserted-by":"publisher","unstructured":"Handley, M.A.T., Vazou, N., Hutton, G.: Liquidate your assets: reasoning about resource usage in liquid haskell. Proc. ACM Program. Lang. 4(POPL), 24:1\u201324:27 (2020). https:\/\/doi.org\/10.1145\/3371092","DOI":"10.1145\/3371092"},{"key":"15_CR23","doi-asserted-by":"publisher","unstructured":"Hicks, M., Bierman, G.M., Guts, N., Leijen, D., Swamy, N.: Polymonadic programming. In: Levy, P.B., Krishnaswami, N. (eds.) Proceedings 5th Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2014, Grenoble, France, 12 April 2014. EPTCS, vol.\u00a0153, pp. 79\u201399 (2014). https:\/\/doi.org\/10.4204\/EPTCS.153.7","DOI":"10.4204\/EPTCS.153.7"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Das, A., Weng, S.C.: Towards automatic resource bound analysis for OCaml. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. pp. 359\u2013373. ACM, Paris France (Jan 2017)","DOI":"10.1145\/3009837.3009842"},{"key":"15_CR25","doi-asserted-by":"publisher","unstructured":"Ivaskovic, A., Mycroft, A., Orchard, D.: Data-flow analyses as effects and graded monads. In: Ariola, Z.M. (ed.) 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference). LIPIcs, vol.\u00a0167, pp. 15:1\u201315:23. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPICS.FSCD.2020.15","DOI":"10.4230\/LIPICS.FSCD.2020.15"},{"key":"15_CR26","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. No.\u00a0141 in Studies in Logic and the Foundations of Mathematics, Elsevier, Amsterdam, paperback ed edn. (2001)"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Katsumata, S.y.: Parametric effect monads and semantics of effect systems. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL \u201914. pp. 633\u2013645. ACM Press, San Diego, California, USA (2014)","DOI":"10.1145\/2535838.2535846"},{"key":"15_CR28","doi-asserted-by":"publisher","unstructured":"Katsumata, S., McDermott, D., Uustalu, T., Wu, N.: Flexible presentations of graded monads. Proc. ACM Program. Lang. 6(ICFP), 902\u2013930 (2022). https:\/\/doi.org\/10.1145\/3547654","DOI":"10.1145\/3547654"},{"key":"15_CR29","doi-asserted-by":"publisher","unstructured":"Kellison, A.E., Hsu, J.: Numerical fuzz: A type system for rounding error analysis. Proc. ACM Program. Lang. 8(PLDI), 1954\u20131978 (2024). https:\/\/doi.org\/10.1145\/3656456","DOI":"10.1145\/3656456"},{"key":"15_CR30","doi-asserted-by":"publisher","unstructured":"Knoth, T., Wang, D., Reynolds, A., Hoffmann, J., Polikarpova, N.: Liquid resource types. Proc. ACM Program. Lang. 4(ICFP), 106:1\u2013106:29 (2020). https:\/\/doi.org\/10.1145\/3408988","DOI":"10.1145\/3408988"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Kura, S.: A General Semantic Construction of Dependent Refinement Type Systems, Categorically. In: Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science, vol. 12650, pp. 406\u2013426. Springer International Publishing (2021)","DOI":"10.1007\/978-3-030-71995-1_21"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"Kura, S., Gaboardi, M., Sekiyama, T., Unno, H.: A category-theoretic framework for dependent effect systems (2026), https:\/\/arxiv.org\/abs\/2601.14846","DOI":"10.1007\/978-3-032-22720-1_15"},{"key":"15_CR33","doi-asserted-by":"crossref","unstructured":"Kura, S., Unno, H.: Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System. Proceedings of the ACM on Programming Languages 8(ICFP), 973\u20131002 (Aug 2024)","DOI":"10.1145\/3674662"},{"key":"15_CR34","doi-asserted-by":"crossref","unstructured":"Levy, P.B., Power, J., Thielecke, H.: Modelling environments in call-by-value programming languages. Information and Computation 185(2), 182\u2013210 (Sep 2003)","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"15_CR35","doi-asserted-by":"crossref","unstructured":"Liell-Cock, J., Staton, S.: Compositional Imprecise Probability: A Solution from Graded Monads and Markov Categories. Proceedings of the ACM on Programming Languages 9(POPL), 1596\u20131626 (Jan 2025)","DOI":"10.1145\/3704890"},{"key":"15_CR36","doi-asserted-by":"publisher","unstructured":"Liu, J., Kretz, I., Liu, H., Tan, B., Wang, J., Sun, Y., Pearson, L., Miltner, A., Dillig, I., Feng, Y.: Certifying zero-knowledge circuits with refinement types. In: IEEE Symposium on Security and Privacy, SP 2024, San Francisco, CA, USA, May 19-23, 2024. pp. 1741\u20131759. IEEE (2024). https:\/\/doi.org\/10.1109\/SP54263.2024.00078","DOI":"10.1109\/SP54263.2024.00078"},{"key":"15_CR37","doi-asserted-by":"publisher","unstructured":"Lobo-Vesga, E., Russo, A., Gaboardi, M., Corti\u00f1as, C.T.: Sensitivity by parametricity. Proc. ACM Program. Lang. 8(OOPSLA2) (Oct 2024). https:\/\/doi.org\/10.1145\/3689726","DOI":"10.1145\/3689726"},{"key":"15_CR38","doi-asserted-by":"publisher","unstructured":"Lucassen, J.M., Gifford, D.K.: Polymorphic effect systems. In: Ferrante, J., Mager, P. (eds.) Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, California, USA, January 10-13, 1988. pp. 47\u201357. ACM Press (1988). https:\/\/doi.org\/10.1145\/73560.73564","DOI":"10.1145\/73560.73564"},{"key":"15_CR39","doi-asserted-by":"publisher","unstructured":"Maillard, K., Ahman, D., Atkey, R., Mart\u00ednez, G., Hritcu, C., Rivas, E., Tanter, \u00c9.: Dijkstra monads for all. Proc. ACM Program. Lang. 3(ICFP), 104:1\u2013104:29 (2019). https:\/\/doi.org\/10.1145\/3341708","DOI":"10.1145\/3341708"},{"key":"15_CR40","doi-asserted-by":"publisher","unstructured":"Marino, D., Millstein, T.D.: A generic type-and-effect system. In: Kennedy, A., Ahmed, A. (eds.) Proceedings of TLDI\u201909: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009. pp. 39\u201350. ACM (2009). https:\/\/doi.org\/10.1145\/1481861.1481868","DOI":"10.1145\/1481861.1481868"},{"key":"15_CR41","volume-title":"Abstraction","author":"A McIver","year":"2005","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science, Springer, New York (2005)"},{"key":"15_CR42","doi-asserted-by":"publisher","unstructured":"Moon, B., III, H.E., Orchard, D.: Graded modal dependent type theory. In: Yoshida, N. (ed.) Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12648, pp. 462\u2013490. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_17","DOI":"10.1007\/978-3-030-72019-3_17"},{"key":"15_CR43","doi-asserted-by":"publisher","unstructured":"Mukai, R., Kobayashi, N., Sato, R.: Parameterized recursive refinement types for automated program verification. In: Singh, G., Urban, C. (eds.) Static Analysis - 29th International Symposium, SAS 2022, Auckland, New Zealand, December 5-7, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13790, pp. 397\u2013421. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-22308-2_18","DOI":"10.1007\/978-3-031-22308-2_18"},{"key":"15_CR44","doi-asserted-by":"crossref","unstructured":"Nanjo, Y., Unno, H., Koskinen, E., Terauchi, T.: A Fixpoint Logic and Dependent Effects for Temporal Property Verification. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science. pp. 759\u2013768. ACM, Oxford United Kingdom (Jul 2018)","DOI":"10.1145\/3209108.3209204"},{"key":"15_CR45","doi-asserted-by":"publisher","unstructured":"Niu, Y., Sterling, J., Grodin, H., Harper, R.: A cost-aware logical framework. Proc. ACM Program. Lang. 6(POPL), 1\u201331 (2022). https:\/\/doi.org\/10.1145\/3498670","DOI":"10.1145\/3498670"},{"key":"15_CR46","doi-asserted-by":"publisher","unstructured":"Orchard, D., Liepelt, V.B., Eades\u00a0III, H.: Quantitative program reasoning with graded modal types. Proc. ACM Program. Lang. 3(ICFP) (Jul 2019). https:\/\/doi.org\/10.1145\/3341714","DOI":"10.1145\/3341714"},{"key":"15_CR47","doi-asserted-by":"publisher","unstructured":"Orchard, D.A., Petricek, T.: Embedding effect systems in haskell. In: Swierstra, W. (ed.) Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, Gothenburg, Sweden, September 4-5, 2014. pp. 13\u201324. ACM (2014). https:\/\/doi.org\/10.1145\/2633357.2633368","DOI":"10.1145\/2633357.2633368"},{"key":"15_CR48","doi-asserted-by":"crossref","unstructured":"P\u00e9drot, P.M., Tabareau, N.: The fire triangle: How to mix substitution, dependent elimination, and effects. Proceedings of the ACM on Programming Languages 4(POPL), 1\u201328 (Jan 2020)","DOI":"10.1145\/3371126"},{"issue":"1","key":"15_CR49","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1023\/A:1023064908962","volume":"11","author":"G Plotkin","year":"2003","unstructured":"Plotkin, G., Power, J.: Algebraic operations and generic effects. Applied Categorical Structures 11(1), 69\u201394 (2003)","journal-title":"Applied Categorical Structures"},{"key":"15_CR50","doi-asserted-by":"crossref","unstructured":"Radi\u010dek, I., Barthe, G., Gaboardi, M., Garg, D., Zuleger, F.: Monadic refinements for relational cost analysis. Proceedings of the ACM on Programming Languages 2(POPL), 1\u201332 (Jan 2018)","DOI":"10.1145\/3158124"},{"key":"15_CR51","doi-asserted-by":"publisher","unstructured":"Rajani, V., Gaboardi, M., Garg, D., Hoffmann, J.: A unifying type-theory for higher-order (amortized) cost analysis. Proc. ACM Program. Lang. 5(POPL), 1\u201328 (2021). https:\/\/doi.org\/10.1145\/3434308","DOI":"10.1145\/3434308"},{"key":"15_CR52","doi-asserted-by":"crossref","unstructured":"Sannier, V., Baillot, P.: Dependent Coeffects for Local Sensitivity Analysis. Proceedings of the ACM on Programming Languages 10(POPL), 806\u2013832 (Jan 2026)","DOI":"10.1145\/3776670"},{"key":"15_CR53","doi-asserted-by":"crossref","unstructured":"Sekiyama, T., Unno, H.: Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations. Proceedings of the ACM on Programming Languages 7(POPL), 2079\u20132110 (Jan 2023)","DOI":"10.1145\/3571264"},{"key":"15_CR54","doi-asserted-by":"crossref","unstructured":"Smirnov, A.L.: Graded monads and rings of polynomials. Journal of Mathematical Sciences 151(3), 3032\u20133051 (Jun 2008)","DOI":"10.1007\/s10958-008-9013-7"},{"key":"15_CR55","doi-asserted-by":"publisher","unstructured":"Swamy, N., Hritcu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P., Kohlweiss, M., Zinzindohoue, J.K., Zanella-B\u00e9guelin, S.: Dependent types and multi-monadic effects in F. In: Bod\u00edk, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. pp. 256\u2013270. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837655","DOI":"10.1145\/2837614.2837655"},{"key":"15_CR56","doi-asserted-by":"publisher","unstructured":"Swamy, N., Weinberger, J., Schlesinger, C., Chen, J., Livshits, B.: Verifying higher-order programs with the dijkstra monad. In: Boehm, H., Flanagan, C. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201913, Seattle, WA, USA, June 16-19, 2013. pp. 387\u2013398. ACM (2013). https:\/\/doi.org\/10.1145\/2491956.2491978","DOI":"10.1145\/2491956.2491978"},{"key":"15_CR57","doi-asserted-by":"publisher","unstructured":"Tate, R.: The sequential semantics of producer effect systems. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 15\u201326. POPL \u201913, Association for Computing Machinery, New York, NY, USA (2013). https:\/\/doi.org\/10.1145\/2429069.2429074","DOI":"10.1145\/2429069.2429074"},{"key":"15_CR58","doi-asserted-by":"publisher","unstructured":"Unno, H., Satake, Y., Terauchi, T.: Relatively complete refinement type system for verification of higher-order non-deterministic programs. Proc. ACM Program. Lang. 2(POPL), 12:1\u201312:29 (2018). https:\/\/doi.org\/10.1145\/3158100","DOI":"10.1145\/3158100"},{"key":"15_CR59","doi-asserted-by":"crossref","unstructured":"V\u00e1k\u00e1r, M., Kammar, O., Staton, S.: A domain theory for statistical probabilistic programming. Proceedings of the ACM on Programming Languages 3(POPL), 1\u201329 (Jan 2019)","DOI":"10.1145\/3290349"},{"key":"15_CR60","doi-asserted-by":"publisher","unstructured":"Vazou, N., Seidel, E.L., Jhala, R.: Liquidhaskell: experience with refinement types in the real world. In: Swierstra, W. (ed.) Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, Gothenburg, Sweden, September 4-5, 2014. pp. 39\u201351. ACM (2014). https:\/\/doi.org\/10.1145\/2633357.2633366","DOI":"10.1145\/2633357.2633366"},{"key":"15_CR61","doi-asserted-by":"publisher","unstructured":"Wang, P., Wang, D., Chlipala, A.: Timl: a functional language for practical complexity analysis with invariants. Proc. ACM Program. Lang. 1(OOPSLA) (Oct 2017). https:\/\/doi.org\/10.1145\/3133903","DOI":"10.1145\/3133903"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22720-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T19:24:46Z","timestamp":1777577086000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22720-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227195","9783032227201"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22720-1_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"10 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}