{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T04:08:55Z","timestamp":1772510935224,"version":"3.50.1"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2022,4,6]],"date-time":"2022-04-06T00:00:00Z","timestamp":1649203200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Villum Investigator","award":["25804"],"award-info":[{"award-number":["25804"]}]},{"name":"Center for Basic Research in Program Verification"},{"DOI":"10.13039\/501100004063","name":"Knut and Alice Wallenberg foundation","doi-asserted-by":"crossref","award":["2020.0266"],"award-info":[{"award-number":["2020.0266"]}],"id":[{"id":"10.13039\/501100004063","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Air Force Office of Scientific Research under MURI","award":["FA9550-15-1-0053 and FA9550-19-1-0216"],"award-info":[{"award-number":["FA9550-15-1-0053 and FA9550-19-1-0216"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2022,7,31]]},"abstract":"<jats:p>Birkedal et al. recently introduced dependent right adjoints as an important class of (non-fibered) modalities in type theory. We observe that several aspects of their calculus are left underdeveloped and that it cannot serve as an internal language. We resolve these problems by assuming that the modal context operator is a parametric right adjoint. We show that this hitherto unrecognized structure is common. Based on these discoveries we present a new well-behaved Fitch-style multimodal type theory, which can be used as an internal language. Finally, we apply this syntax to guarded recursion and parametricity.<\/jats:p>","DOI":"10.1145\/3514241","type":"journal-article","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T11:41:29Z","timestamp":1648554089000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Modalities and Parametric Adjoints"],"prefix":"10.1145","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1944-0789","authenticated-orcid":false,"given":"Daniel","family":"Gratzer","sequence":"first","affiliation":[{"name":"Aarhus University, Aabogade, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Evan","family":"Cavallo","sequence":"additional","affiliation":[{"name":"Stockholm University, Stockholm, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G. A.","family":"Kavvos","sequence":"additional","affiliation":[{"name":"University of Bristol, Bristol, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adrien","family":"Guatto","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Paris, CNRS, IRIF, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Aabogade, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,4,6]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500597"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/2060081"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000268"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005097"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341713"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434283"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.006"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005291931660"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129519000197"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.27"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49630-5_2"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001183"},{"key":"e_1_3_3_15_2","volume-title":"Generalised Algebraic Theories and Contextual Categories","author":"Cartmell John","year":"1978","unstructured":"John Cartmell. 1978. Generalised Algebraic Theories and Contextual Categories. Ph.D. Dissertation. University of Oxford."},{"key":"e_1_3_3_16_2","volume-title":"Higher Inductive Types and Internal Parametricity for Cubical Type Theory","author":"Cavallo Evan","year":"2021","unstructured":"Evan Cavallo. 2021. Higher Inductive Types and Internal Parametricity for Cubical Type Theory. Ph.D. Dissertation. Carnegie Mellon University."},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2020.13"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:8)2012"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_14"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_26"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_66"},{"key":"e_1_3_3_22_2","doi-asserted-by":"crossref","unstructured":"Marcelo Fiore. 2012. Discrete generalised polynomial functors. Retrieved from https:\/\/www.cl.cam.ac.uk\/mpf23\/talks\/ICALP2012.pdf.","DOI":"10.1007\/978-3-642-31585-5_22"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394736"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:11)2021"},{"key":"e_1_3_3_25_2","unstructured":"Daniel Gratzer G. A. Kavvos Andreas Nuyts and Lars Birkedal. 2020. Type theory \u00e0 la mode. Retrieved from https:\/\/jozefg.github.io\/papers\/type-theory-a-la-mode.pdf."},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341711"},{"key":"e_1_3_3_27_2","doi-asserted-by":"crossref","unstructured":"Daniel Gratzer Jonathan Sterling and Lars Birkedal. 2019. Normalization-by-evaluation for modal dependent type theory. Retrieved from https:\/\/jozefg.github.io\/papers\/2019-implementing-modal-dependent-type-theory-tech-report.pdf.","DOI":"10.1145\/3341711"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526619.004"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290315"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-27683-0_16"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2017.25"},{"key":"e_1_3_3_32_2","article-title":"Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory","volume":"16","author":"Mannaa Bassel","year":"2020","unstructured":"Bassel Mannaa, Rasmus Ejlers M\u00f8gelberg, and Niccol\u00f2 Veltri. 2020. Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory. Logic. Methods Comput. Sci. 16, 4 (December 2020).","journal-title":"Logic. Methods Comput. Sci."},{"key":"e_1_3_3_33_2","unstructured":"Luca Mauri. 2017. Algebraic theories in monoidal categories. arxiv:math.LO\/1705.09202. Retrieved from https:\/\/arxiv.org\/abs\/1705.09202."},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.5555\/788022.789002"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"e_1_3_3_36_2","unstructured":"Emily Riehl and Michael Shulman. A type theory for synthetic  \\( \\infty \\) -categories."},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000147"},{"key":"e_1_3_3_38_2","unstructured":"Thomas Streicher. 2020. Fibred categories \u00e0 la Jean B\u00e9nabou. arXiv:1801.02927. Retrieved from https:\/\/arxiv.org\/abs\/1801.02927."},{"key":"e_1_3_3_39_2","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"Program The Univalent Foundations","year":"2013","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study."},{"key":"e_1_3_3_40_2","first-page":"1181","article-title":"A C-system defined by a universe category","volume":"30","author":"Voevodsky Vladimir","year":"2015","unstructured":"Vladimir Voevodsky. 2015. A C-system defined by a universe category. Theory Appl. Categor. 30 (2015), 1181\u20131214.","journal-title":"Theory Appl. Categor."},{"key":"e_1_3_3_41_2","first-page":"665","article-title":"Familial 2-functors and parametric right adjoints","volume":"18","author":"Weber Mark","year":"2007","unstructured":"Mark Weber. 2007. Familial 2-functors and parametric right adjoints. Theory Appl. Categor. 18 (2007), 665\u2013732.","journal-title":"Theory Appl. Categor."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3514241","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3514241","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:10:14Z","timestamp":1750183814000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3514241"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,6]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,7,31]]}},"alternative-id":["10.1145\/3514241"],"URL":"https:\/\/doi.org\/10.1145\/3514241","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,6]]},"assertion":[{"value":"2021-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-04-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}