{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:33:05Z","timestamp":1767929585254,"version":"3.49.0"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2021,7,28]],"date-time":"2021-07-28T00:00:00Z","timestamp":1627430400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We introduce MTT, a dependent type theory which supports multiple modalities.\nMTT is parametrized by a mode theory which specifies a collection of modes,\nmodalities, and transformations between them. We show that different choices of\nmode theory allow us to use the same type theory to compute and reason in many\nmodal situations, including guarded recursion, axiomatic cohesion, and\nparametric quantification. We reproduce examples from prior work in guarded\nrecursion and axiomatic cohesion, thereby demonstrating that MTT constitutes a\nsimple and usable syntax whose instantiations intuitively correspond to\nprevious handcrafted modal type theories. In some cases, instantiating MTT to a\nparticular situation unearths a previously unknown type theory that improves\nupon prior systems. Finally, we investigate the metatheory of MTT. We prove the\nconsistency of MTT and establish canonicity through an extension of recent\ntype-theoretic gluing techniques. These results hold irrespective of the choice\nof mode theory, and thus apply to a wide variety of modal situations.<\/jats:p>","DOI":"10.46298\/lmcs-17(3:11)2021","type":"journal-article","created":{"date-parts":[[2021,7,30]],"date-time":"2021-07-30T19:45:25Z","timestamp":1627674325000},"source":"Crossref","is-referenced-by-count":20,"title":["Multimodal Dependent Type Theory"],"prefix":"10.46298","volume":"Volume 17, Issue 3","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1944-0789","authenticated-orcid":false,"given":"Daniel","family":"Gratzer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G. A.","family":"Kavvos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1571-5063","authenticated-orcid":false,"given":"Andreas","family":"Nuyts","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2021,7,28]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/7713\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/7713\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:20:06Z","timestamp":1687292406000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/7571"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,28]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-17(3:11)2021","relation":{"has-preprint":[{"id-type":"arxiv","id":"2011.15021v2","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2011.15021","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2011.15021","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,7,28]]},"article-number":"7571"}}