{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:14:23Z","timestamp":1775790863566,"version":"3.50.1"},"publisher-location":"Cham","reference-count":55,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720186","type":"print"},{"value":"9783030720193","type":"electronic"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Deductive verification techniques based on program logics (i.e., the family of Floyd-Hoare logics) are a powerful approach for program reasoning. Recently, there has been a trend of increasing the expressive power of such logics by augmenting their rules with additional information to reason about program side-effects. For example, general program logics have been augmented with cost analyses, logics for probabilistic computations have been augmented with estimate measures, and logics for differential privacy with indistinguishability bounds. In this work, we unify these various approaches via the paradigm of <jats:italic>grading<\/jats:italic>, adapted from the world of functional calculi and semantics. We propose <jats:italic>Graded Hoare Logic<\/jats:italic> (GHL), a parameterisable framework for augmenting program logics with a preordered monoidal analysis. We develop a semantic framework for modelling GHL such that grading, logical assertions (pre- and post-conditions) and the underlying effectful semantics of an imperative language can be integrated together. Central to our framework is the notion of a <jats:italic>graded category<\/jats:italic> which we extend here, introducing <jats:italic>graded Freyd categories<\/jats:italic> which provide a semantics that can interpret many examples of augmented program logics from the literature. We leverage coherent fibrations to model the base assertion language, and thus the overall setting is also fibrational.<\/jats:p>","DOI":"10.1007\/978-3-030-72019-3_9","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T14:03:10Z","timestamp":1616421790000},"page":"234-263","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Graded Hoare Logic and its Categorical Semantics"],"prefix":"10.1007","author":[{"given":"Marco","family":"Gaboardi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7529-5489","authenticated-orcid":false,"given":"Shin-ya","family":"Katsumata","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7058-7842","authenticated-orcid":false,"given":"Dominic","family":"Orchard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9895-9209","authenticated-orcid":false,"given":"Tetsuya","family":"Sato","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","unstructured":"Atkey, R.: Parameterised notions of computation. J. Funct. Program. 19(3-4), 335\u2013376 (2009). https:\/\/doi.org\/10.1017\/S095679680900728X","DOI":"10.1017\/S095679680900728X"},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.: Proving differential privacy via probabilistic couplings. In: 2016 31st Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). pp. 1\u201310 (2016). https:\/\/doi.org\/10.1145\/2933575.2934554","DOI":"10.1145\/2933575.2934554"},{"key":"9_CR3","unstructured":"Barthe, G.: An introduction to relational program verification (2020), http:\/\/software.imdea.org\/~gbarthe\/__introrelver.pdf, working Draft"},{"key":"9_CR4","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gaboardi, M., Arias, E.J.G., Hsu, J., Roth, A., Strub, P.: Higher-order approximate relational refinement types for mechanism design and differential privacy. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. pp. 55\u201368. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2677000","DOI":"10.1145\/2676726.2677000"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.: A Program Logic for Union Bounds. In: 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy. pp. 107:1\u2013107:15 (2016). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2016.107","DOI":"10.4230\/LIPIcs.ICALP.2016.107"},{"key":"9_CR6","doi-asserted-by":"publisher","unstructured":"Barthe, G., K\u00f6pf, B., Olmedo, F., Zanella-B\u00e9guelin, S.: Probabilistic relational reasoning for differential privacy. ACM Trans. Progr. Lang. Syst. 35(3), 9:1\u20139:49 (Nov 2013). https:\/\/doi.org\/10.1145\/2492061","DOI":"10.1145\/2492061"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Brunel, A., Gaboardi, M., Mazza, D., Zdancewic, S.: A core quantitative coeffect calculus. In: Shao, Z. (ed.) Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. Lecture Notes in Computer Science, vol.\u00a08410, pp. 351\u2013370. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_19","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"9_CR8","doi-asserted-by":"publisher","unstructured":"Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015. pp. 467\u2013478 (2015). https:\/\/doi.org\/10.1145\/2737924.2737955","DOI":"10.1145\/2737924.2737955"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Crole, R.L.: Categories for types. Cambridge University Press (1993)","DOI":"10.1017\/CBO9781139172707"},{"key":"9_CR10","unstructured":"Day, B.: Construction of Biclosed Categories. Ph.D. thesis, School of Mathematics of the University of New South Wales (1970)"},{"key":"9_CR11","unstructured":"Filinski, A.: Controlling Effects. Ph.D. thesis, Carnegie Mellon University (1996)"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Floyd, R.W.: Assigning meanings to programs. Proceedings of Symposium on Applied Mathematics 19, 19\u201332 (1967). https:\/\/doi.org\/10.1007\/978-94-011-1793-7_4","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"9_CR13","doi-asserted-by":"publisher","unstructured":"Fujii, S., Katsumata, S.y., Mellies, P.A.: Towards a formal theory of graded monads. In: International Conference on Foundations of Software Science and Computation Structures. 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":"9_CR14","unstructured":"Gaboardi, M., Katsumata, S., Orchard, D., Sato, T.: Graded Hoare Logic and its Categorical Semantics. CoRR abs\/2007.11235 (2020), https:\/\/arxiv.org\/abs\/2007.11235"},{"key":"9_CR15","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":"9_CR16","doi-asserted-by":"publisher","unstructured":"Ghica, D.R., Smith, A.I.: Bounded linear types in a resource semiring. In: Shao, Z. (ed.) Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. Lecture Notes in Computer Science, vol.\u00a08410, pp. 331\u2013350. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_18","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"9_CR17","doi-asserted-by":"publisher","unstructured":"Gibbons, J.: Comprehending ringads - for phil wadler, on the occasion of his 60th birthday. In: Lindley, S., McBride, C., Trinder, P.W., Sannella, D. (eds.) A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 9600, pp. 132\u2013151. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-30936-1_7","DOI":"10.1007\/978-3-319-30936-1_7"},{"key":"9_CR18","doi-asserted-by":"publisher","unstructured":"Goncharov, S., Schr\u00f6der, L.: A Relatively Complete Generic Hoare Logic for Order-Enriched Effects. In: 28th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013. pp. 273\u2013282. IEEE Computer Society (2013). https:\/\/doi.org\/10.1109\/LICS.2013.33","DOI":"10.1109\/LICS.2013.33"},{"key":"9_CR19","doi-asserted-by":"publisher","unstructured":"Goubault-Larrecq, J., Lasota, S., Nowak, D.: Logical relations for monadic types. Mathematical Structures in Computer Science 18(6), 1169\u20131217 (2008). https:\/\/doi.org\/10.1017\/S0960129508007172","DOI":"10.1017\/S0960129508007172"},{"key":"9_CR20","doi-asserted-by":"publisher","unstructured":"Hasuo, I.: Generic weakest precondition semantics from monads enriched with order. Theoretical Computer Science 604, 2 \u2013 29 (2015). https:\/\/doi.org\/10.1016\/j.tcs.2015.03.047, coalgebraic Methods in Computer Science","DOI":"10.1016\/j.tcs.2015.03.047"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Iva\u0161kovi\u0107, 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). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0167, pp. 15:1\u201315:23. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2020). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2020.15","DOI":"10.4230\/LIPIcs.FSCD.2020.15"},{"key":"9_CR22","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Elsevier (1999)"},{"key":"9_CR23","doi-asserted-by":"publisher","unstructured":"Jacobs, B.: Dijkstra and Hoare monads in monadic computation. Theor. Comput. Sci. 604, 30\u201345 (2015). https:\/\/doi.org\/10.1016\/j.tcs.2015.03.020","DOI":"10.1016\/j.tcs.2015.03.020"},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Katsumata, S.: Parametric effect monads and semantics of effect systems. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914, San Diego, CA, USA, January 20-21, 2014. pp. 633\u2013646. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535846","DOI":"10.1145\/2535838.2535846"},{"key":"9_CR25","doi-asserted-by":"publisher","unstructured":"Katsumata, S.: A Double Category Theoretic Analysis of Graded Linear Exponential Comonads. In: Baier, C., Lago, U.D. (eds.) Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10803, pp. 110\u2013127. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89366-2_6","DOI":"10.1007\/978-3-319-89366-2_6"},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Katsumata, S., Sato, T., Uustalu, T.: Codensity lifting of monads and its dual. Logical Methods in Computer Science 14(4) (2018). https:\/\/doi.org\/10.23638\/LMCS-14(4:6)2018","DOI":"10.23638\/LMCS-14(4:6)2018"},{"key":"9_CR27","doi-asserted-by":"publisher","unstructured":"Kura, S.: Graded Algebraic Theories. In: International Conference on Foundations of Software Science and Computation Structures. pp. 401\u2013421. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45231-5_21","DOI":"10.1007\/978-3-030-45231-5_21"},{"key":"9_CR28","unstructured":"Levy, P.B.: Locally graded categories. Slides available at http:\/\/www.cs.bham.ac.uk\/~pbl\/papers\/locgrade.pdf (2019)"},{"key":"9_CR29","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":"9_CR30","doi-asserted-by":"publisher","unstructured":"Maillard, K., Hritcu, C., Rivas, E., Muylder, A.V.: The next 700 relational program logics. Proc. ACM Program. Lang. 4(POPL), 4:1\u20134:33 (2020). https:\/\/doi.org\/10.1145\/3371072","DOI":"10.1145\/3371072"},{"key":"9_CR31","doi-asserted-by":"publisher","unstructured":"Martin, U., Mathiesen, E.A., Oliva, P.: Hoare Logic in the Abstract. In: \u00c9sik, Z. (ed.) Computer Science Logic. pp. 501\u2013515. Springer Berlin Heidelberg, Berlin, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11874683_33","DOI":"10.1007\/11874683_33"},{"key":"9_CR32","doi-asserted-by":"publisher","unstructured":"Melli\u00e8s, P., Zeilberger, N.: Functors are Type Refinement Systems. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. pp. 3\u201316. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676970","DOI":"10.1145\/2676726.2676970"},{"key":"9_CR33","doi-asserted-by":"publisher","unstructured":"Milius, S., Pattinson, D., Schr\u00f6der, L.: Generic Trace Semantics and Graded Monads. In: Moss, L.S., Sobocinski, P. (eds.) 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a035, pp. 253\u2013269. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik (2015). https:\/\/doi.org\/10.4230\/LIPIcs.CALCO.2015.253","DOI":"10.4230\/LIPIcs.CALCO.2015.253"},{"key":"9_CR34","doi-asserted-by":"publisher","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55\u201392 (1991). https:\/\/doi.org\/10.1016\/0890-5401(91)90052-4","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"9_CR35","doi-asserted-by":"publisher","unstructured":"Molnar, D., Piotrowski, M., Schultz, D., Wagner, D.A.: The program counter security model: Automatic detection and removal of control-flow side channel attacks. In: Won, D., Kim, S. (eds.) Information Security and Cryptology - ICISC 2005, 8th International Conference, Seoul, Korea, December 1-2, 2005, Revised Selected Papers. Lecture Notes in Computer Science, vol.\u00a03935, pp. 156\u2013168. Springer (2005). https:\/\/doi.org\/10.1007\/11734727_14","DOI":"10.1007\/11734727_14"},{"key":"9_CR36","doi-asserted-by":"publisher","unstructured":"Mycroft, A., Orchard, D.A., Petricek, T.: Effect Systems Revisited - Control-Flow Algebra and Semantics. In: Probst, C.W., Hankin, C., Hansen, R.R. (eds.) Semantics, Logics, and Calculi - Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays. Lecture Notes in Computer Science, vol.\u00a09560, pp. 1\u201332. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-27810-0_1","DOI":"10.1007\/978-3-319-27810-0_1"},{"key":"9_CR37","doi-asserted-by":"publisher","unstructured":"Nielson, H.R.: A Hoare-like proof system for analysing the computation time of programs. Science of Computer Programming 9(2), 107\u2013136 (1987). https:\/\/doi.org\/10.1016\/0167-6423(87)90029-3","DOI":"10.1016\/0167-6423(87)90029-3"},{"key":"9_CR38","unstructured":"Nielson, H.R., Nielson, F.: Semantics with applications, vol.\u00a0104. Springer (1992)"},{"key":"9_CR39","unstructured":"Olmedo, F.: Approximate Relational Reasoning for Probabilistic Programs. Ph.D. thesis, Technical University of Madrid (2014)"},{"key":"9_CR40","doi-asserted-by":"publisher","unstructured":"Orchard, D., Liepelt, V., III, H.E.: Quantitative program reasoning with graded modal types. Proc. ACM Program. Lang. 3(ICFP), 110:1\u2013110:30 (2019). https:\/\/doi.org\/10.1145\/3341714","DOI":"10.1145\/3341714"},{"key":"9_CR41","doi-asserted-by":"publisher","unstructured":"Orchard, D., Wadler, P., III, H.E.: Unifying graded and parameterised monads. In: New, M.S., Lindley, S. (eds.) Proceedings Eighth Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2020, Dublin, Ireland, 25th April 2020. EPTCS, vol.\u00a0317, pp. 18\u201338 2020). https:\/\/doi.org\/10.4204\/EPTCS.317.2","DOI":"10.4204\/EPTCS.317.2"},{"key":"9_CR42","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":"9_CR43","doi-asserted-by":"publisher","unstructured":"Petricek, T., Orchard, D.A., Mycroft, A.: Coeffects: Unified static analysis of context-dependence. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M.Z., Peleg, D. (eds.) Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II. Lecture Notes in Computer Science, vol.\u00a07966, pp. 385\u2013397. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39212-2_35","DOI":"10.1007\/978-3-642-39212-2_35"},{"key":"9_CR44","doi-asserted-by":"publisher","unstructured":"Petricek, T., Orchard, D.A., Mycroft, A.: Coeffects: a calculus of context-dependent computation. In: Jeuring, J., Chakravarty, M.M.T. (eds.) Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014. pp. 123\u2013135. ACM (2014). https:\/\/doi.org\/10.1145\/2628136.2628160","DOI":"10.1145\/2628136.2628160"},{"key":"9_CR45","unstructured":"Pitts, A.M.: Categorical logic. Tech. rep., University of Cambridge, Computer Laboratory (1995)"},{"key":"9_CR46","doi-asserted-by":"publisher","unstructured":"Power, J.: Generic models for computational effects. Theoretical Computer Science 364(2), 254\u2013269 (2006). https:\/\/doi.org\/10.1016\/j.tcs.2006.08.006","DOI":"10.1016\/j.tcs.2006.08.006"},{"key":"9_CR47","doi-asserted-by":"crossref","unstructured":"Power, J., Thielecke, H.: Environments, continuation semantics and indexed categories. In: Abadi, M., Ito, T. (eds.) Theoretical Aspects of Computer Software. pp. 391\u2013414. Springer Berlin Heidelberg, Berlin, Heidelberg (1997)","DOI":"10.1007\/BFb0014560"},{"key":"9_CR48","doi-asserted-by":"publisher","unstructured":"Sato, T.: Approximate Relational Hoare Logic for Continuous Random Samplings. In: Birkedal, L. (ed.) The Thirty-second Conference on the Mathematical Foundations of Programming Semantics, MFPS 2016, Carnegie Mellon University, Pittsburgh, PA, USA, May 23-26, 2016. Electronic Notes in Theoretical Computer Science, vol.\u00a0325, pp. 277\u2013298. Elsevier (2016). https:\/\/doi.org\/10.1016\/j.entcs.2016.09.043","DOI":"10.1016\/j.entcs.2016.09.043"},{"key":"9_CR49","doi-asserted-by":"publisher","unstructured":"Sato, T., Barthe, G., Gaboardi, M., Hsu, J., Katsumata, S.: Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy. In: 34th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019. pp. 1\u201314 (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785668","DOI":"10.1109\/LICS.2019.8785668"},{"key":"9_CR50","doi-asserted-by":"publisher","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","DOI":"10.1007\/s10958-008-9013-7"},{"key":"9_CR51","doi-asserted-by":"publisher","unstructured":"Staton, S.: Freyd categories are Enriched Lawvere Theories. Electronic Notes in Theoretical Computer Science 303, 197 \u2013 206 (2014). https:\/\/doi.org\/10.1016\/j.entcs.2014.02.010, proceedings of the Workshop on Algebra, Coalgebra and Topology (WACT 2013)","DOI":"10.1016\/j.entcs.2014.02.010"},{"key":"9_CR52","doi-asserted-by":"publisher","unstructured":"Staton, S.: Commutative semantics for probabilistic programming. In: Yang, H. (ed.) Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10201, pp. 855\u2013879. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_32","DOI":"10.1007\/978-3-662-54434-1_32"},{"key":"9_CR53","doi-asserted-by":"publisher","unstructured":"Tate, R.: The sequential semantics of producer effect systems. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy - January 23 - 25, 2013. pp. 15\u201326. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429074","DOI":"10.1145\/2429069.2429074"},{"key":"9_CR54","doi-asserted-by":"publisher","unstructured":"Wood, R.J.: V-indexed categories, chap.\u00a02, pp. 126\u2013140. No.\u00a0661 in Lecture Notes in Mathematics, Springer (1978). https:\/\/doi.org\/10.1007\/BFb0061362","DOI":"10.1007\/BFb0061362"},{"key":"9_CR55","doi-asserted-by":"publisher","unstructured":"Zhang, J.J.: Twisted graded algebras and equivalences of graded categories. Proceedings of the London Mathematical Society 3(2), 281\u2013311 (1996). https:\/\/doi.org\/10.1112\/plms\/s3-72.2.281","DOI":"10.1112\/plms\/s3-72.2.281"}],"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-030-72019-3_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,25]],"date-time":"2021-10-25T03:05:48Z","timestamp":1635131148000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-72019-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720186","9783030720193"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72019-3_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","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":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","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":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"79","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference took place virtually due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}