{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,20]],"date-time":"2026-04-20T22:41:01Z","timestamp":1776724861878,"version":"3.51.2"},"reference-count":48,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2019,12,12]],"date-time":"2019-12-12T00:00:00Z","timestamp":1576108800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2020,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In recent years, we have seen several new models of dependent type theory extended with some form of modal necessity operator, including nominal type theory, guarded and clocked type theory and spatial and cohesive type theory. In this paper, we study <jats:italic>modal dependent type theory<\/jats:italic>: dependent type theory with an operator satisfying (a dependent version of) the K axiom of modal logic. We investigate both semantics and syntax. For the semantics, we introduce categories with families with a <jats:italic>dependent right adjoint<\/jats:italic> (CwDRA) and show that the examples above can be presented as such. Indeed, we show that any category with finite limits and an adjunction of endofunctors give rise to a CwDRA via the local universe construction. For the syntax, we introduce a dependently typed extension of Fitch-style modal <jats:italic>\u03bb<\/jats:italic>-calculus, show that it can be interpreted in any CwDRA, and build a term model. We extend the syntax and semantics with universes.<\/jats:p>","DOI":"10.1017\/s0960129519000197","type":"journal-article","created":{"date-parts":[[2019,12,12]],"date-time":"2019-12-12T09:43:11Z","timestamp":1576143791000},"page":"118-138","source":"Crossref","is-referenced-by-count":21,"title":["Modal dependent type theory and dependent right adjoints"],"prefix":"10.1017","volume":"30","author":[{"given":"Lars","family":"Birkedal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ranald","family":"Clouston","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0097-6188","authenticated-orcid":false,"given":"Bassel","family":"Mannaa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rasmus","family":"Ejlers M\u00f8gelberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7775-3471","authenticated-orcid":false,"given":"Andrew M.","family":"Pitts","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bas","family":"Spitters","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2019,12,12]]},"reference":[{"key":"S0960129519000197_ref19","unstructured":"Coquand, T. (2012). Presheaf model of type theory. Unpublished note. www.cse.chalmers.se\/~coquand\/presheaf.pdf"},{"key":"S0960129519000197_ref35","unstructured":"Mannaa, B. and M\u00f8gelberg, R. E. (2018). The clocks they are adjunctions denotational semantics for clocked type theory. In: 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9\u201312, 2018, Oxford, UK, 23:1\u201323:17."},{"key":"S0960129519000197_ref26","unstructured":"Hofmann, M. (1997). Syntax and semantics of dependent types. In: Extensional Constructs in Intensional Type Theory, Springer, 13\u201354."},{"key":"S0960129519000197_ref14","article-title":"Undecidability of equality in the free locally cartesian closed category (extended version)","volume":"13","author":"Castellan","year":"2017","journal-title":"LMCS"},{"key":"S0960129519000197_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_14"},{"key":"S0960129519000197_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500597"},{"key":"S0960129519000197_ref18","unstructured":"Cohen, C. , Coquand, T. , Huber, S. and M\u00f6rtberg, A. (2018). Cubical type theory: A constructive interpretation of the univalence axiom. In: Uustalu, T. (ed.) 21st International Conference on Types for Proofs and Programs (TYPES 2015), Vol. 69. Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 5:1\u20135:34."},{"key":"S0960129519000197_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2016.06.010"},{"key":"S0960129519000197_ref45","unstructured":"Streicher, T. (1993). Investigations into intensional type theory, Habilitation thesis, Ludwig Maximilian Universit\u00e4t."},{"key":"S0960129519000197_ref11","author":"Blackburn","year":"2002"},{"key":"S0960129519000197_ref43","unstructured":"Rijke, E. , Shulman, M. and Spitters, B. (2018). Modalities in homotopy type theory. LMCS."},{"key":"S0960129519000197_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_26"},{"key":"S0960129519000197_ref31","volume-title":"3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018","author":"Licata","year":"2018"},{"key":"S0960129519000197_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676969"},{"key":"S0960129519000197_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49630-5_2"},{"key":"S0960129519000197_ref41","author":"Pitts","year":"2013"},{"key":"S0960129519000197_ref47","unstructured":"Voevodsky, V. (2014). A C-system defined by a universe category, arXiv:1409.7925."},{"key":"S0960129519000197_ref7","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.27"},{"key":"S0960129519000197_ref33","unstructured":"Lumsdaine, P. L. and Warren, M. A. (2015). The local universes model: An overlooked coherence construction for dependent type theories. ACM Trans. Comput. Logic 16 (3), 23:1\u201323:31."},{"key":"S0960129519000197_ref6","unstructured":"Birkedal, L. , Bizjak, A. , Clouston, R. , Grathwohl, H. B. , Spitters, B. and Vezzosi, A. (2018). Guarded cubical type theory. Journal of Automated Reasoning."},{"key":"S0960129519000197_ref46","unstructured":"V\u00e1k\u00e1r, M. (2017). In search of effectful dependent types, PhD thesis, University of Oxford."},{"key":"S0960129519000197_ref3","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005097"},{"key":"S0960129519000197_ref32","unstructured":"Licata, D. R. , Shulman, M. and Riley, M. (2017). A fibrational framework for substructural and modal logics. In: LIPIcs-Leibniz International Proceedings in Informatics, Vol. 84, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"S0960129519000197_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"S0960129519000197_ref38","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855774"},{"key":"S0960129519000197_ref40","unstructured":"Nuyts, A. , Vezzosi, A. and Devriese, D. (2017). Parametric quantifiers for dependent type theory. PACMPL 1 (ICFP), 32:1\u201332:29."},{"key":"S0960129519000197_ref10","unstructured":"Bizjak, A. and M\u00f8gelberg, R. (2018). Denotational semantics for guarded dependent type theory, arXiv:1802.03744."},{"key":"S0960129519000197_ref8","first-page":"1","article-title":"First steps in synthetic guarded domain theory: Step-indexing in the topos of trees","volume":"8","author":"Birkedal","year":"2012","journal-title":"LMCS"},{"key":"S0960129519000197_ref22","unstructured":"Dybjer, P. (1995). Internal type theory. In: International Workshop on Types for Proofs and Programs, Springer, 120\u2013134."},{"key":"S0960129519000197_ref25","unstructured":"Hofmann, M. (1994). On the interpretation of type theory in locally cartesian closed categories. In: International Workshop on Computer Science Logic, Springer, 427\u2013441."},{"key":"S0960129519000197_ref42","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.04.003"},{"key":"S0960129519000197_ref37","unstructured":"M\u00f8gelberg, R. E. (2014). A type theory for productive coprogramming via guarded recursion. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, Vienna, Austria, July 14\u201318, 2014, 71:1\u201371:10."},{"key":"S0960129519000197_ref34","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39193"},{"key":"S0960129519000197_ref27","volume-title":"Sketches of An Elephant: A Topos Theory Compendium","author":"Johnstone","year":"2002"},{"key":"S0960129519000197_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-2798-3_12"},{"key":"S0960129519000197_ref44","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000147"},{"key":"S0960129519000197_ref23","volume-title":"Symbolic Logic, An Introduction","author":"Fitch","year":"1952"},{"key":"S0960129519000197_ref24","first-page":"2666","article-title":"Cohomologie non ab\u00e9lienne","volume":"260","author":"Giraud","year":"1965","journal-title":"C. R. Acad. Sci. Paris"},{"key":"S0960129519000197_ref29","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005089"},{"key":"S0960129519000197_ref13","unstructured":"Castellan, S. (2014). Dependent type theory as the initial category with families, Technical report, Chalmers University of Technology. Internship Report. http:\/\/iso.mor.phis.me\/archives\/2011-2012\/stage-2012-goteburg\/report.pdf"},{"key":"S0960129519000197_ref12","unstructured":"Borghuis, V. A. J. (1994). Coming to terms with modal logic: on the interpretation of modalities in typed lambda-calculus, PhD thesis, Technische Universiteit Eindhoven."},{"key":"S0960129519000197_ref48","unstructured":"Wellen, F. (2017). Formalizing Cartan Geometry in Modal Homotopy Type Theory, PhD thesis, Karlsruher Institut f\u00fcr Technologie."},{"key":"S0960129519000197_ref39","unstructured":"Norell, U. (2007). Towards a practical programming language based on dependent type theory, PhD thesis, Chalmers University of Technology."},{"key":"S0960129519000197_ref2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/14.4.447"},{"key":"S0960129519000197_ref15","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000881"},{"key":"S0960129519000197_ref4","unstructured":"Bellin, G. , De Paiva, V. and Ritter, E. (2001). Extended curry-howard correspondence for a basic constructive modal logic. In: Proceedings of Methods for Modalities."},{"key":"S0960129519000197_ref5","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005291931660"},{"key":"S0960129519000197_ref28","unstructured":"Kapulkin, C. and Lumsdaine, P. L. (2018). The simplicial model of univalent foundations (after Voedodsky). Journal of the European Mathematical Society. To appear."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129519000197","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,20]],"date-time":"2020-10-20T08:28:24Z","timestamp":1603182504000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129519000197\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,12]]},"references-count":48,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,2]]}},"alternative-id":["S0960129519000197"],"URL":"https:\/\/doi.org\/10.1017\/s0960129519000197","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,12]]}}}