{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:04:55Z","timestamp":1784232295734,"version":"3.55.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["2006535"],"award-info":[{"award-number":["2006535"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>\n            Dependency analysis is vital to several applications in computer science. It lies at the essence of secure information flow analysis, binding-time analysis, etc. Various calculi have been proposed in the literature for analysing individual dependencies. Abadi et. al., by extending Moggi\u2019s monadic metalanguage, unified several of these calculi into the Dependency Core Calculus (DCC). DCC has served as a foundational framework for dependency analysis for the last two decades. However, in spite of its success, DCC has its limitations. First, the monadic bind rule of the calculus is nonstandard and relies upon an auxiliary protection judgement. Second, being of a monadic nature, the calculus cannot capture dependency analyses that possess a comonadic nature, for example, the binding-time calculus, \u03bb\n            <jats:sup>\u2218<\/jats:sup>\n            , of Davies. In this paper, we address these limitations by designing an alternative dependency calculus that is inspired by standard ideas from category theory. Our calculus is both monadic and comonadic in nature and subsumes both DCC and \u03bb\n            <jats:sup>\u2218<\/jats:sup>\n            . Our construction explains the nonstandard bind rule and the protection judgement of DCC in terms of standard categorical concepts. It also leads to a novel technique for proving correctness of dependency analysis. We use this technique to present alternative proofs of correctness for DCC and \u03bb\n            <jats:sup>\u2218<\/jats:sup>\n            .\n          <\/jats:p>","DOI":"10.1145\/3563335","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"1320-1348","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Monadic and comonadic aspects of dependency analysis"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0432-7820","authenticated-orcid":false,"given":"Pritam","family":"Choudhury","sequence":"first","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292555"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3264820.3264823"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341693"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2858949.2784733"},{"key":"e_1_2_1_5_1","volume-title":"Computational Comonads and Intensional Semantics","author":"Brookes Stephen","unstructured":"Stephen Brookes and Shai Geva . 1991. Computational Comonads and Intensional Semantics . Cambridge Univ. Press , 1\u201344. Stephen Brookes and Shai Geva. 1991. Computational Comonads and Intensional Semantics. Cambridge Univ. Press, 1\u201344."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_2_1_7_1","volume-title":"Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection","author":"Calcagno Cristiano","unstructured":"Cristiano Calcagno , Walid Taha , Liwen Huang , and Xavier Leroy . 2003. Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection . In Generative Programming and Component Engineering, Frank Pfenning and Yannis Smaragdakis (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 57\u201376. isbn:978-3-540-39815-8 Cristiano Calcagno, Walid Taha, Liwen Huang, and Xavier Leroy. 2003. Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection. In Generative Programming and Component Engineering, Frank Pfenning and Yannis Smaragdakis (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 57\u201376. isbn:978-3-540-39815-8"},{"key":"#cr-split#-e_1_2_1_8_1.1","unstructured":"Pritam Choudhury. 2022. Monadic and Comonadic Aspects of Dependency Analysis. https:\/\/doi.org\/10.48550\/ARXIV.2209.06334 10.48550\/ARXIV.2209.06334"},{"key":"#cr-split#-e_1_2_1_8_1.2","doi-asserted-by":"crossref","unstructured":"Pritam Choudhury. 2022. Monadic and Comonadic Aspects of Dependency Analysis. https:\/\/doi.org\/10.48550\/ARXIV.2209.06334","DOI":"10.1145\/3563335"},{"key":"e_1_2_1_9_1","volume-title":"A Dependent Dependency Calculus","author":"Choudhury Pritam","unstructured":"Pritam Choudhury , Harley Eades , and Stephanie Weirich . 2022. A Dependent Dependency Calculus . In Programming Languages and Systems, Ilya Sergey (Ed.). Springer International Publishing , Cham . 403\u2013430. isbn:978-3-030-99336-8 Pritam Choudhury, Harley Eades, and Stephanie Weirich. 2022. A Dependent Dependency Calculus. In Programming Languages and Systems, Ilya Sergey (Ed.). Springer International Publishing, Cham. 403\u2013430. isbn:978-3-030-99336-8"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3011069"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360056"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/359636.359712"},{"key":"e_1_2_1_13_1","volume-title":"Closed Categories. In Proceedings of the Conference on Categorical Algebra, S. Eilenberg, D. K. Harrison, S. MacLane, and H. R\u00f6hrl (Eds.). Springer Berlin Heidelberg","author":"Eilenberg Samuel","unstructured":"Samuel Eilenberg and G. Max Kelly . 1966 . Closed Categories. In Proceedings of the Conference on Categorical Algebra, S. Eilenberg, D. K. Harrison, S. MacLane, and H. R\u00f6hrl (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg. 421\u2013562. isbn:978-3-642-99902-4 Samuel Eilenberg and G. Max Kelly. 1966. Closed Categories. In Proceedings of the Conference on Categorical Algebra, S. Eilenberg, D. K. Harrison, S. MacLane, and H. R\u00f6hrl (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 421\u2013562. isbn:978-3-642-99902-4"},{"key":"e_1_2_1_14_1","unstructured":"Soichiro Fujii. 2019. A 2-Categorical Study of Graded and Indexed Monads. arxiv:1904.08083. \t\t\t\t  Soichiro Fujii. 2019. A 2-Categorical Study of Graded and Indexed Monads. arxiv:1904.08083."},{"key":"e_1_2_1_15_1","volume-title":"Smith","author":"Ghica Dan R.","year":"2014","unstructured":"Dan R. Ghica and Alex I . Smith . 2014 . Bounded Linear Types in a Resource Semiring. In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg. 331\u2013350. isbn:978-3-642-54833-8 Dan R. Ghica and Alex I. Smith. 2014. Bounded Linear Types in a Resource Semiring. In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 331\u2013350. isbn:978-3-642-54833-8"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/319838.319848"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/646445.692151"},{"key":"e_1_2_1_18_1","volume-title":"Security Policies and Security Models. In 1982 IEEE Symposium on Security and Privacy. 11\u201311","author":"Goguen J. A.","unstructured":"J. A. Goguen and J. Meseguer . 1982 . Security Policies and Security Models. In 1982 IEEE Symposium on Security and Privacy. 11\u201311 . J. A. Goguen and J. Meseguer. 1982. Security Policies and Security Models. In 1982 IEEE Symposium on Security and Privacy. 11\u201311."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000058"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002405"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268976"},{"key":"e_1_2_1_22_1","volume-title":"Categorical Logic and Type Theory","author":"Jacobs Bart","unstructured":"Bart Jacobs . 1999. Categorical Logic and Type Theory . Elsevier , Amsterdam, The Netherlands. Bart Jacobs. 1999. Categorical Logic and Type Theory. Elsevier, Amsterdam, The Netherlands."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535846"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290333"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01220868"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01304852"},{"key":"e_1_2_1_27_1","volume-title":"Categories for the Working Mathematician","author":"MacLane Saunders","unstructured":"Saunders MacLane . 1971. Categories for the Working Mathematician . Springer-Verlag , New York . Graduate Texts in Mathematics, Vol. 5 . Saunders MacLane. 1971. Categories for the Working Mathematician. Springer-Verlag, New York. Graduate Texts in Mathematics, Vol. 5."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/647163.717695"},{"key":"e_1_2_1_30_1","volume-title":"Coeffects: Unified Static Analysis of Context-Dependence. In Automata, Languages, and Programming","author":"Petricek Tomas","year":"2013","unstructured":"Tomas Petricek , Dominic Orchard , and Alan Mycroft . 2013 . Coeffects: Unified Static Analysis of Context-Dependence. In Automata, Languages, and Programming . Springer Berlin Heidelberg, Berlin , Heidelberg . 385\u2013397. isbn:978-3-642-39212-2 Tomas Petricek, Dominic Orchard, and Alan Mycroft. 2013. Coeffects: Unified Static Analysis of Context-Dependence. In Automata, Languages, and Programming. Springer Berlin Heidelberg, Berlin, Heidelberg. 385\u2013397. isbn:978-3-642-39212-2"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1782734.1782758"},{"key":"e_1_2_1_33_1","volume-title":"Principles of Secure Information Flow Analysis","author":"Smith Geoffrey","unstructured":"Geoffrey Smith . 2007. Principles of Secure Information Flow Analysis . In Malware Detection, Mihai Christodorescu, Somesh Jha, Douglas Maughan, Dawn Song, and Cliff Wang (Eds.). Springer US , Boston, MA . 291\u2013307. isbn:978-0-387-44599-1 Geoffrey Smith. 2007. Principles of Secure Information Flow Analysis. In Malware Detection, Mihai Christodorescu, Somesh Jha, Douglas Maughan, Dawn Song, and Cliff Wang (Eds.). Springer US, Boston, MA. 291\u2013307. isbn:978-0-387-44599-1"},{"key":"e_1_2_1_34_1","volume-title":"Effect Systems with Subtyping. In In ACM Conference on Partial Evaluation and Program Manipulation. ACM Press, 45\u201353","author":"Tang Yan Mei","year":"1995","unstructured":"Yan Mei Tang and Pierre Jouvelot . 1995 . Effect Systems with Subtyping. In In ACM Conference on Partial Evaluation and Program Manipulation. ACM Press, 45\u201353 . Yan Mei Tang and Pierre Jouvelot. 1995. Effect Systems with Subtyping. In In ACM Conference on Partial Evaluation and Program Manipulation. ACM Press, 45\u201353."},{"key":"e_1_2_1_35_1","first-page":"121","article-title":"A Survey of Program Slicing Techniques","volume":"3","author":"Tip Frank","year":"1995","unstructured":"Frank Tip . 1995 . A Survey of Program Slicing Techniques . Journal of Programming Languages , 3 (1995), 121 \u2013 189 . Frank Tip. 1995. A Survey of Program Slicing Techniques. Journal of Programming Languages, 3 (1995), 121\u2013189.","journal-title":"Journal of Programming Languages"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016850.1016868"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.05.029"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/353629.353648"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/601775.601776"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563335","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563335","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563335","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:10Z","timestamp":1750178290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563335"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":41,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563335"],"URL":"https:\/\/doi.org\/10.1145\/3563335","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}