Modalities and Parametric Adjoints
| Autor: | Daniel Gratzer, Evan Cavallo, G. A. Kavvos, Adrien Guatto, Lars Birkedal |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2022 |
| Předmět: | |
| Zdroj: | Gratzer, D, Cavallo, E, Kavvos, G A, Guatto, A & Birkedal, L 2022, ' Modalities and Parametric Adjoints ', ACM Transactions on Computational Logic, vol. 23, no. 3, 18, pp. 1-29 . https://doi.org/10.1145/3514241 Gratzer, D, Cavallo, E, Kavvos, G A, Guatto, A & Birkedal, L 2022, ' Modalities and Parametric Adjoints ', ACM Transactions on Computational Logic, vol. 23, no. 3, 18 . https://doi.org/10.1145/3514241 |
| DOI: | 10.1145/3514241 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|