Multimodal Dependent Type Theory
We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and re...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2021-07-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/7571/pdf |
| _version_ | 1797268469124694016 |
|---|---|
| author | Daniel Gratzer G. A. Kavvos Andreas Nuyts Lars Birkedal |
| author_facet | Daniel Gratzer G. A. Kavvos Andreas Nuyts Lars Birkedal |
| author_sort | Daniel Gratzer |
| collection | DOAJ |
| description | We introduce MTT, a dependent type theory which supports multiple modalities.
MTT is parametrized by a mode theory which specifies a collection of modes,
modalities, and transformations between them. We show that different choices of
mode theory allow us to use the same type theory to compute and reason in many
modal situations, including guarded recursion, axiomatic cohesion, and
parametric quantification. We reproduce examples from prior work in guarded
recursion and axiomatic cohesion, thereby demonstrating that MTT constitutes a
simple and usable syntax whose instantiations intuitively correspond to
previous handcrafted modal type theories. In some cases, instantiating MTT to a
particular situation unearths a previously unknown type theory that improves
upon prior systems. Finally, we investigate the metatheory of MTT. We prove the
consistency of MTT and establish canonicity through an extension of recent
type-theoretic gluing techniques. These results hold irrespective of the choice
of mode theory, and thus apply to a wide variety of modal situations. |
| first_indexed | 2024-04-25T01:32:58Z |
| format | Article |
| id | doaj.art-07e0c9691a85467f9ebe85fa9649460a |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:32:58Z |
| publishDate | 2021-07-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-07e0c9691a85467f9ebe85fa9649460a2024-03-08T10:35:15ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742021-07-01Volume 17, Issue 310.46298/lmcs-17(3:11)20217571Multimodal Dependent Type TheoryDaniel Gratzerhttps://orcid.org/0000-0003-1944-0789G. A. KavvosAndreas Nuytshttps://orcid.org/0000-0002-1571-5063Lars BirkedalWe introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and reason in many modal situations, including guarded recursion, axiomatic cohesion, and parametric quantification. We reproduce examples from prior work in guarded recursion and axiomatic cohesion, thereby demonstrating that MTT constitutes a simple and usable syntax whose instantiations intuitively correspond to previous handcrafted modal type theories. In some cases, instantiating MTT to a particular situation unearths a previously unknown type theory that improves upon prior systems. Finally, we investigate the metatheory of MTT. We prove the consistency of MTT and establish canonicity through an extension of recent type-theoretic gluing techniques. These results hold irrespective of the choice of mode theory, and thus apply to a wide variety of modal situations.https://lmcs.episciences.org/7571/pdfcomputer science - logic in computer science |
| spellingShingle | Daniel Gratzer G. A. Kavvos Andreas Nuyts Lars Birkedal Multimodal Dependent Type Theory Logical Methods in Computer Science computer science - logic in computer science |
| title | Multimodal Dependent Type Theory |
| title_full | Multimodal Dependent Type Theory |
| title_fullStr | Multimodal Dependent Type Theory |
| title_full_unstemmed | Multimodal Dependent Type Theory |
| title_short | Multimodal Dependent Type Theory |
| title_sort | multimodal dependent type theory |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/7571/pdf |
| work_keys_str_mv | AT danielgratzer multimodaldependenttypetheory AT gakavvos multimodaldependenttypetheory AT andreasnuyts multimodaldependenttypetheory AT larsbirkedal multimodaldependenttypetheory |