{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T14:17:40Z","timestamp":1787062660824,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":69,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032081865","type":"print"},{"value":"9783032081872","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,25]],"date-time":"2025-11-25T00:00:00Z","timestamp":1764028800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,25]],"date-time":"2025-11-25T00:00:00Z","timestamp":1764028800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-08187-2_7","type":"book-chapter","created":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T05:43:13Z","timestamp":1763962993000},"page":"114-148","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["On Graded Coeffect Types for\u00a0Information-Flow Control"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2198-1819","authenticated-orcid":false,"given":"Vilem-Benjamin","family":"Liepelt","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4284-3757","authenticated-orcid":false,"given":"Danielle","family":"Marshall","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7058-7842","authenticated-orcid":false,"given":"Dominic","family":"Orchard","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7701-8311","authenticated-orcid":false,"given":"Vineet","family":"Rajani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0496-8268","authenticated-orcid":false,"given":"Michael","family":"Vollmer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,11,25]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Abadi, M., Banerjee, A., Heintze, N., Riecke, J.G.: A core calculus of dependency. In: Appel, A.W., Aiken, A. (eds.) POPL 1999, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, 20\u201322 January 1999, pp. 147\u2013160. ACM (1999). https:\/\/doi.org\/10.1145\/292540.292555","DOI":"10.1145\/292540.292555"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Abel, A., Bernardy, J.: A unified view of modalities in type systems. Proc. ACM Program. Lang. 4(ICFP), 90:1\u201390:28 (2020). https:\/\/doi.org\/10.1145\/3408972","DOI":"10.1145\/3408972"},{"key":"7_CR3","doi-asserted-by":"publisher","unstructured":"Abel, A., Danielsson, N.A., Eriksson, O.: A graded modal dependent type theory with a universe and erasure, formalized. Proc. ACM Program. Lang. 7(ICFP), 920\u2013954 (2023). https:\/\/doi.org\/10.1145\/3607862","DOI":"10.1145\/3607862"},{"key":"7_CR4","unstructured":"Abera, T., Yitayew, Y., Wasihun, D., Kolluru, V.: Ordered weak idempotent rings. Palest. J. Math. 13(3) (2024)"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Algehed, M.: A perspective on the dependency core calculus. In: Alvim, M.S., Delaune, S. (eds.) Proceedings of the 13th Workshop on Programming Languages and Analysis for Security, PLAS@CCS 2018, Toronto, ON, Canada, 15\u201319 October 2018, pp. 24\u201328. ACM (2018). https:\/\/doi.org\/10.1145\/3264820.3264823","DOI":"10.1145\/3264820.3264823"},{"key":"7_CR6","doi-asserted-by":"publisher","unstructured":"Atkey, R.: Syntax and semantics of quantitative type theory. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, 09\u201312 2018, pp. 56\u201365. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209189","DOI":"10.1145\/3209108.3209189"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/3-540-56992-8_6","volume-title":"Computer Science Logic","author":"N Benton","year":"1993","unstructured":"Benton, N., Bierman, G., de Paiva, V., Hyland, M.: Linear $$\\lambda $$-calculus and categorical models revisited. In: B\u00f6rger, E., J\u00e4ger, G., Kleine B\u00fcning, H., Martini, S., Richter, M.M. (eds.) CSL 1992. LNCS, vol. 702, pp. 61\u201384. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56992-8_6"},{"key":"7_CR8","doi-asserted-by":"publisher","unstructured":"Bernardy, J., Boespflug, M., Newton, R.R., Jones, S.P., Spiwack, A.: Linear Haskell: practical linearity in a higher-order polymorphic language. Proc. ACM Program. Lang. 2(POPL), 5:1\u20135:29 (2018). https:\/\/doi.org\/10.1145\/3158093","DOI":"10.1145\/3158093"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Bianchini, R., Dagnino, F., Giannini, P., Zucca, E.: A Java-like calculus with heterogeneous coeffects. Theor. Comput. Sci. 971, 114063 (2023). https:\/\/doi.org\/10.1016\/J.TCS.2023.114063","DOI":"10.1016\/J.TCS.2023.114063"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Bianchini, R., Dagnino, F., Giannini, P., Zucca, E.: Multi-graded featherweight Java. In: Ali, K., Salvaneschi, G. (eds.) 37th European Conference on Object-Oriented Programming, ECOOP 2023, Seattle, Washington, United States, 17\u201321 July 2023. LIPIcs, vol.\u00a0263, pp. 3:1\u20133:27. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2023.3","DOI":"10.4230\/LIPICS.ECOOP.2023.3"},{"key":"7_CR11","unstructured":"Bierman, G.M., De\u00a0Paiva, V.C.: Intuitionistic necessity revisited. School of Computer Science research reports-University of Birmingham CSR (1996)"},{"issue":"3","key":"7_CR12","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1023\/A:1005291931660","volume":"65","author":"GM Bierman","year":"2000","unstructured":"Bierman, G.M., de Paiva, V.: On an intuitionistic modal logic. Stud. Logica. 65(3), 383\u2013416 (2000). https:\/\/doi.org\/10.1023\/A:1005291931660","journal-title":"Stud. Logica."},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"Brady, E.C.: Idris 2: quantitative type theory in practice. In: M\u00f8ller, A., Sridharan, M. (eds.) 35th European Conference on Object-Oriented Programming, ECOOP 2021, Aarhus, Denmark,, 11\u201317 July 2021 (Virtual Conference). LIPIcs, vol.\u00a0194, pp. 9:1\u20139:26. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2021.9","DOI":"10.4230\/LIPICS.ECOOP.2021.9"},{"key":"7_CR14","volume-title":"Computational comonads and intensional semantics","author":"S Brookes","year":"1991","unstructured":"Brookes, S., Geva, S.: Computational comonads and intensional semantics. Carnegie-Mellon University, Department of Computer Science (1991)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-54833-8_19","volume-title":"Programming Languages and Systems","author":"A Brunel","year":"2014","unstructured":"Brunel, A., Gaboardi, M., Mazza, D., Zdancewic, S.: A core quantitative coeffect calculus. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 351\u2013370. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_19"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"Buiras, P., Vytiniotis, D., Russo, A.: HLIO: mixing static and dynamic typing for information-flow control in Haskell. In: Fisher, K., Reppy, J.H. (eds.) Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, 1\u20133 September 2015, pp. 289\u2013301. ACM (2015). https:\/\/doi.org\/10.1145\/2784731.2784758","DOI":"10.1145\/2784731.2784758"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Choudhury, P.: Monadic and comonadic aspects of dependency analysis. Proc. ACM Program. Lang. 6(OOPSLA2), 1320\u20131348 (2022). https:\/\/doi.org\/10.1145\/3563335","DOI":"10.1145\/3563335"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Choudhury, P., III, H.E., Eisenberg, R.A., Weirich, S.: A graded dependent type system with a usage-aware semantics. Proc. ACM Program. Lang. 5(POPL), 1\u201332 (2021). https:\/\/doi.org\/10.1145\/3434331","DOI":"10.1145\/3434331"},{"issue":"5","key":"7_CR19","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"DE Denning","year":"1976","unstructured":"Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236\u2013243 (1976). https:\/\/doi.org\/10.1145\/360051.360056","journal-title":"Commun. ACM"},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"Gaboardi, M., Haeberlen, A., Hsu, J., Narayan, A., Pierce, B.C.: Linear dependent types for differential privacy. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Rome, Italy, 23\u201325 January 2013, pp. 357\u2013370. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429113","DOI":"10.1145\/2429069.2429113"},{"key":"7_CR21","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, 18\u201322 September 2016, pp. 476\u2013489. ACM (2016). https:\/\/doi.org\/10.1145\/2951913.2951939","DOI":"10.1145\/2951913.2951939"},{"issue":"1","key":"7_CR22","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1017\/S0956796809990268","volume":"20","author":"SJ Gay","year":"2010","unstructured":"Gay, S.J., Vasconcelos, V.T.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19\u201350 (2010). https:\/\/doi.org\/10.1017\/S0956796809990268","journal-title":"J. Funct. Program."},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-642-54833-8_18","volume-title":"Programming Languages and Systems","author":"DR Ghica","year":"2014","unstructured":"Ghica, D.R., Smith, A.I.: Bounded linear types in a resource semiring. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 331\u2013350. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_18"},{"key":"7_CR24","doi-asserted-by":"publisher","unstructured":"Gifford, D.K., Lucassen, J.M.: Integrating functional and imperative programming. In: Scherlis, W.L., Williams, J.H., Gabriel, R.P. (eds.) Proceedings of the 1986 ACM Conference on LISP and Functional Programming, LFP 1986, Cambridge, Massachusetts, USA, 4\u20136 August 1986, pp. 28\u201338. ACM (1986). https:\/\/doi.org\/10.1145\/319838.319848","DOI":"10.1145\/319838.319848"},{"issue":"1","key":"7_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"JY Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. Theoret. Comput. Sci. 50(1), 1\u2013101 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"7_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(92)90386-T","volume":"97","author":"J Girard","year":"1992","unstructured":"Girard, J., Scedrov, A., Scott, P.J.: Bounded linear logic: a modular approach to polynomial-time computability. Theor. Comput. Sci. 97(1), 1\u201366 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90386-T","journal-title":"Theor. Comput. Sci."},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"Hainry, E., P\u00e9choux, R.: A type-based complexity analysis of object oriented programs. Inf. Comput. 261, 78\u2013115 (2018). https:\/\/doi.org\/10.1016\/J.IC.2018.05.006","DOI":"10.1016\/J.IC.2018.05.006"},{"key":"7_CR28","doi-asserted-by":"publisher","unstructured":"Hedin, D., Sabelfeld, A.: A perspective on information-flow control. In: Nipkow, T., Grumberg, O., Hauptmann, B. (eds.) Software Safety and Security - Tools for Analysis and Verification, NATO Science for Peace and Security Series - D: Information and Communication Security, vol.\u00a033, pp. 319\u2013347. IOS Press (2012). https:\/\/doi.org\/10.3233\/978-1-61499-028-4-319","DOI":"10.3233\/978-1-61499-028-4-319"},{"key":"7_CR29","doi-asserted-by":"publisher","unstructured":"Heintze, N., Riecke, J.G.: The slam calculus: programming with secrecy and integrity. In: MacQueen, D.B., Cardelli, L. (eds.) POPL 1998, Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, 19\u201321 January 1998, pp. 365\u2013377. ACM (1998). https:\/\/doi.org\/10.1145\/268946.268976","DOI":"10.1145\/268946.268976"},{"key":"7_CR30","doi-asserted-by":"publisher","unstructured":"Hughes, J., Orchard, D.: Resourceful program synthesis from graded linear types. In: Fern\u00e1ndez, M. (ed.) Logic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Bologna, Italy, 7\u20139 September 2020, Proceedings. LNCS, vol. 12561, pp. 151\u2013170. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-68446-4_8","DOI":"10.1007\/978-3-030-68446-4_8"},{"key":"7_CR31","doi-asserted-by":"publisher","unstructured":"Hughes, J., Orchard, D.: Program synthesis from graded types. In: Weirich, S. (ed.) Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, 6\u201311 April 2024, Proceedings, Part I. LNCS, vol. 14576, pp. 83\u2013112. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57262-3_4","DOI":"10.1007\/978-3-031-57262-3_4"},{"key":"7_CR32","doi-asserted-by":"publisher","unstructured":"Hughes, J., Vollmer, M., Orchard, D.: Deriving distributive laws for graded linear types. In: Lago, U.D., de\u00a0Paiva, V. (eds.) Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity &TLLA@IJCAR-FSCD 2020, Online, 29\u201330 June 2020. EPTCS, vol.\u00a0353, pp. 109\u2013131 (2020). https:\/\/doi.org\/10.4204\/EPTCS.353.6","DOI":"10.4204\/EPTCS.353.6"},{"key":"7_CR33","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 2014, San Diego, CA, USA, 20\u201321 January 2014, pp. 633\u2013646. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535846","DOI":"10.1145\/2535838.2535846"},{"key":"7_CR34","doi-asserted-by":"publisher","unstructured":"Lago, U.D., Gaboardi, M.: Linear dependent types and relative completeness. Log. Methods Comput. Sci. 8(4) (2011). https:\/\/doi.org\/10.2168\/LMCS-8(4:11)2012","DOI":"10.2168\/LMCS-8(4:11)2012"},{"key":"7_CR35","unstructured":"Liepelt, V.B., Orchard, D., Marshall, D.: Same coeffect, different base: graded types with and without linearity (2024, under review)"},{"key":"7_CR36","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, 10\u201313 January 1988, pp. 47\u201357. ACM Press (1988). https:\/\/doi.org\/10.1145\/73560.73564","DOI":"10.1145\/73560.73564"},{"key":"7_CR37","unstructured":"Marshall, D., Orchard, D.: Graded modal types for integrity and confidentiality. In: 17th Workshop on Programming Languages and Analysis for Security (PLAS 2022) (2022). https:\/\/arxiv.org\/abs\/2309.04324"},{"key":"7_CR38","doi-asserted-by":"publisher","unstructured":"Marshall, D., Orchard, D.: Functional ownership through fractional uniqueness. Proc. ACM Program. Lang. 8(OOPSLA1), 1040\u20131070 (2024). https:\/\/doi.org\/10.1145\/3649848","DOI":"10.1145\/3649848"},{"key":"7_CR39","doi-asserted-by":"publisher","unstructured":"Marshall, D., Orchard, D.: Non-linear communication via graded modal session types. Inf. Comput. 301, 105234 (2024). https:\/\/doi.org\/10.1016\/J.IC.2024.105234","DOI":"10.1016\/J.IC.2024.105234"},{"key":"7_CR40","doi-asserted-by":"publisher","unstructured":"Marshall, D., Vollmer, M., Orchard, D.: Linearity and uniqueness: an entente cordiale. In: Sergey, I. (ed.) Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, 2\u20137 April 2022, Proceedings. LNCS, vol. 13240, pp. 346\u2013375. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99336-8_13","DOI":"10.1007\/978-3-030-99336-8_13"},{"key":"7_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-319-30936-1_12","volume-title":"A List of Successes That Can Change the World","author":"C McBride","year":"2016","unstructured":"McBride, C.: I got plenty o\u2019 Nuttin\u2019. In: Lindley, S., McBride, C., Trinder, P., Sannella, D. (eds.) A List of Successes That Can Change the World. LNCS, vol. 9600, pp. 207\u2013233. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30936-1_12"},{"key":"7_CR42","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":"7_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-030-72019-3_17","volume-title":"Programming Languages and Systems","author":"B Moon","year":"2021","unstructured":"Moon, B., Eades III, H., Orchard, D.: Graded modal dependent type theory. In: ESOP 2021. LNCS, vol. 12648, pp. 462\u2013490. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_17"},{"key":"7_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-27810-0_1","volume-title":"Semantics, Logics, and Calculi","author":"A Mycroft","year":"2016","unstructured":"Mycroft, A., Orchard, D., Petricek, T.: Effect systems revisited\u2014control-flow algebra and semantics. In: Probst, C.W., Hankin, C., Hansen, R.R. (eds.) Semantics, Logics, and Calculi. LNCS, vol. 9560, pp. 1\u201332. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-27810-0_1"},{"key":"7_CR45","doi-asserted-by":"publisher","unstructured":"Myers, A.C.: JFlow: practical mostly-static information flow control. In: Appel, A.W., Aiken, A. (eds.) POPL 1999, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, 20\u201322 January 1999, pp. 228\u2013241. ACM (1999). https:\/\/doi.org\/10.1145\/292540.292561","DOI":"10.1145\/292540.292561"},{"key":"7_CR46","doi-asserted-by":"publisher","unstructured":"Orchard, D., Liepelt, V., III, H.E.: Quantitative program reasoning with graded modal types. PACMPL 3(ICFP), 110:1\u2013110:30 (2019). https:\/\/doi.org\/10.1145\/3341714","DOI":"10.1145\/3341714"},{"key":"7_CR47","unstructured":"Orchard, D.A.: Programming contextual computations. Technical report, University of Cambridge (2014). https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.708000"},{"key":"7_CR48","doi-asserted-by":"publisher","unstructured":"Orchard, D.A., Bolingbroke, M., Mycroft, A.: Ypnos: declarative, parallel structured grid programming. In: Petersen, L., Pontelli, E. (eds.) Proceedings of the POPL 2010 Workshop on Declarative Aspects of Multicore Programming, DAMP 2010, Madrid, Spain, 19 January 2010, pp. 15\u201324. ACM (2010). https:\/\/doi.org\/10.1145\/1708046.1708053","DOI":"10.1145\/1708046.1708053"},{"key":"7_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-41582-1_1","volume-title":"Implementation and Application of Functional Languages","author":"D Orchard","year":"2013","unstructured":"Orchard, D., Mycroft, A.: A notation for comonads. In: Hinze, R. (ed.) IFL 2012. LNCS, vol. 8241, pp. 1\u201317. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41582-1_1"},{"key":"7_CR50","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":"7_CR51","unstructured":"Petricek, T.: Context-aware programming languages. Ph.D. thesis, University of Cambridge (2017)"},{"key":"7_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-642-39212-2_35","volume-title":"Automata, Languages, and Programming","author":"T Petricek","year":"2013","unstructured":"Petricek, T., Orchard, D., Mycroft, A.: Coeffects: unified static analysis of context-dependence. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 385\u2013397. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39212-2_35"},{"key":"7_CR53","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, 1\u20133 September 2014, pp. 123\u2013135. ACM (2014). https:\/\/doi.org\/10.1145\/2628136.2628160","DOI":"10.1145\/2628136.2628160"},{"issue":"1","key":"7_CR54","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/596980.596983","volume":"25","author":"F Pottier","year":"2003","unstructured":"Pottier, F., Simonet, V.: Information flow inference for ML. ACM Trans. Program. Lang. Syst. 25(1), 117\u2013158 (2003). https:\/\/doi.org\/10.1145\/596980.596983","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR55","doi-asserted-by":"publisher","unstructured":"Rajani, V., Garg, D.: Types for information flow control: labeling granularity and semantic models. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, 9\u201312 July 2018, pp. 233\u2013246. IEEE Computer Society (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00024","DOI":"10.1109\/CSF.2018.00024"},{"key":"7_CR56","doi-asserted-by":"publisher","unstructured":"Rajani, V., Garg, D.: On the expressiveness and semantics of information flow types. J. Comput. Secur. 28(1), 129\u2013156 (2020). https:\/\/doi.org\/10.3233\/JCS-191382","DOI":"10.3233\/JCS-191382"},{"key":"7_CR57","doi-asserted-by":"publisher","unstructured":"Russo, A.: Functional pearl: two can keep a secret, if one of them uses Haskell. In: Fisher, K., Reppy, J.H. (eds.) Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, 1\u20133 September 2015, pp. 280\u2013288. ACM (2015). https:\/\/doi.org\/10.1145\/2784731.2784756","DOI":"10.1145\/2784731.2784756"},{"key":"7_CR58","unstructured":"Simonet, V., Rocquencourt, I.: Flow Caml in a nutshell. In: Proceedings of the First APPSEM-II Workshop, pp. 152\u2013165 (2003)"},{"key":"7_CR59","unstructured":"Snider, D., et al.: HHVM and Hack User Documentation. https:\/\/web.archive.org\/web\/20240824005941\/https:\/\/docs.hhvm.com\/hack\/contexts-and-capabilities\/introduction"},{"key":"7_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/11575467_2","volume-title":"Programming Languages and Systems","author":"T Uustalu","year":"2005","unstructured":"Uustalu, T., Vene, V.: The essence of dataflow programming. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 2\u201318. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11575467_2"},{"issue":"7","key":"7_CR61","doi-asserted-by":"publisher","first-page":"1310","DOI":"10.3217\/JUCS-011-07-1311","volume":"11","author":"T Uustalu","year":"2005","unstructured":"Uustalu, T., Vene, V.: Signals and comonads. J. Univers. Comput. Sci. 11(7), 1310\u20131326 (2005). https:\/\/doi.org\/10.3217\/JUCS-011-07-1311","journal-title":"J. Univers. Comput. Sci."},{"key":"7_CR62","doi-asserted-by":"publisher","unstructured":"Uustalu, T., Vene, V.: Comonadic notions of computation. In: Ad\u00e1mek, J., Kupke, C. (eds.) Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science, CMCS 2008, Budapest, Hungary, 4\u20136 April 2008. Electronic Notes in Theoretical Computer Science, vol.\u00a0203, pp. 263\u2013284. Elsevier (2008). https:\/\/doi.org\/10.1016\/J.ENTCS.2008.05.029","DOI":"10.1016\/J.ENTCS.2008.05.029"},{"key":"7_CR63","doi-asserted-by":"publisher","unstructured":"Vollmer, V., Marshall, D., Eades\u00a0III, H., Orchard, D.: A mixed linear and graded logic: proofs, terms and models. In: 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025) (2025). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2025.32","DOI":"10.4230\/LIPIcs.CSL.2025.32"},{"issue":"2\/3","key":"7_CR64","doi-asserted-by":"publisher","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","volume":"4","author":"DM Volpano","year":"1996","unstructured":"Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2\/3), 167\u2013188 (1996). https:\/\/doi.org\/10.3233\/JCS-1996-42-304","journal-title":"J. Comput. Secur."},{"key":"7_CR65","doi-asserted-by":"publisher","unstructured":"Volpano, D.M., Smith, G.: Verifying secrets and relative secrecy. In: POPL 2000, Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, USA, 19\u201321 January 2000, pp. 268\u2013276 (2000). https:\/\/doi.org\/10.1145\/325694.325729","DOI":"10.1145\/325694.325729"},{"key":"7_CR66","unstructured":"Wadler, P.: Linear types can change the world! In: Broy, M., Jones, C.B. (eds.) Programming Concepts and Methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 2\u20135 April 1990, p.\u00a0561. North-Holland (1990)"},{"issue":"1","key":"7_CR67","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. ACM Trans. Comput. Log. 4(1), 1\u201332 (2003). https:\/\/doi.org\/10.1145\/601775.601776","journal-title":"ACM Trans. Comput. Log."},{"key":"7_CR68","doi-asserted-by":"crossref","unstructured":"Walker, D.: Substructural type systems. Adv. Top. Types Program. Lang., 3\u201344 (2005)","DOI":"10.7551\/mitpress\/1104.003.0003"},{"key":"7_CR69","doi-asserted-by":"publisher","unstructured":"Wood, J., Atkey, R.: A linear algebra approach to linear metatheory 353, 195\u2013212 (2020). https:\/\/doi.org\/10.4204\/EPTCS.353.10","DOI":"10.4204\/EPTCS.353.10"}],"container-title":["Lecture Notes in Computer Science","Languages, Compilers, Analysis - From Beautiful Theory to Useful Practice"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-08187-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T13:22:26Z","timestamp":1783516946000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-08187-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,25]]},"ISBN":["9783032081865","9783032081872"],"references-count":69,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-08187-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,25]]},"assertion":[{"value":"25 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}