Modalities and Parametric Adjoints

Daniel Gratzer; Evan Cavallo; G. A. Kavvos; Adrien Guatto; Lars Birkedal

doi:10.1145/3514241

Modalities and Parametric Adjoints

Daniel Gratzer^*, Evan Cavallo, G. A. Kavvos, Adrien Guatto, Lars Birkedal

^*Corresponding author for this work

Department of Computer Science

Research output: Contribution to journal › Article (Academic Journal) › peer-review

5 Citations (Scopus)

363 Downloads (Pure)

Abstract

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.

Original language	English
Article number	18
Pages (from-to)	1-29
Journal	ACM Transactions on Computational Logic
Volume	23
Issue number	3
Early online date	6 Apr 2022
DOIs	https://doi.org/10.1145/3514241
Publication status	Published - 31 Jul 2022

Bibliographical note

Funding Information:
The first, third, and fifth authors were supported in part by a Villum Investigator grant (no. 25804), Center for Basic Research in Program Verification (CPV), from the VILLUM Foundation. The second author was supported in part by the Knut and Alice Wallenberg foundation (no. 2020.0266) and the Air Force Office of Scientific Research under MURI grants FA9550-15-1-0053 and FA9550-19-1-0216. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of any sponsoring institution, the U.S. government, or any other entity. Authors’ addresses: D. Gratzer and L. Birkedal, Aarhus University, Aabogade 34, Aarhus, Denmark, 8200; emails: {gratzer, birkedal}@cs.au.dk; E. Cavallo, Stockholm University, SE-106 91, Stockholm, Sweden; email: [email protected]; G. A. Kavvos, University of Bristol, Merchant Venturers Building, Bristol, United Kingdom, BS8 1UB; email: alex.kavvos @bristol.ac.uk; A. Guatto, Université de Paris, CNRS, IRIF, F-75006, Paris, France; email: [email protected]. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]. © 2022 Copyright held by the owner/author(s). Publication rights licensed to ACM. 1529-3785/2022/04-ART18 $15.00 https://doi.org/10.1145/3514241

Publisher Copyright:
© 2022 Copyright held by the owner/author(s). Publication rights licensed to ACM.

Research Groups and Themes

Programming Languages

Keywords

modal logic
category theory
type theory

Access to Document

10.1145/3514241

Full-text PDF (final published version)
This is the final published version of the article (version of record). It first appeared online via ACM at https://doi.org/10.1145/3514241. Please refer to any applicable terms of use of the publisher.
Accepted author manuscript, 815 KB

Handle.net

Persistent link

Cite this

@article{ea431b5e58424714ae0c801d55ad2aa9,

title = "Modalities and Parametric Adjoints",

abstract = "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.",

keywords = "modal logic, category theory, type theory",

author = "Daniel Gratzer and Evan Cavallo and Kavvos, {G. A.} and Adrien Guatto and Lars Birkedal",

note = "Funding Information: The first, third, and fifth authors were supported in part by a Villum Investigator grant (no. 25804), Center for Basic Research in Program Verification (CPV), from the VILLUM Foundation. The second author was supported in part by the Knut and Alice Wallenberg foundation (no. 2020.0266) and the Air Force Office of Scientific Research under MURI grants FA9550-15-1-0053 and FA9550-19-1-0216. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of any sponsoring institution, the U.S. government, or any other entity. Authors{\textquoteright} addresses: D. Gratzer and L. Birkedal, Aarhus University, Aabogade 34, Aarhus, Denmark, 8200; emails: {gratzer, birkedal}@cs.au.dk; E. Cavallo, Stockholm University, SE-106 91, Stockholm, Sweden; email: [email protected]; G. A. Kavvos, University of Bristol, Merchant Venturers Building, Bristol, United Kingdom, BS8 1UB; email: alex.kavvos @bristol.ac.uk; A. Guatto, Universit{\'e} de Paris, CNRS, IRIF, F-75006, Paris, France; email: [email protected]. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]. {\textcopyright} 2022 Copyright held by the owner/author(s). Publication rights licensed to ACM. 1529-3785/2022/04-ART18 $15.00 https://doi.org/10.1145/3514241 Publisher Copyright: {\textcopyright} 2022 Copyright held by the owner/author(s). Publication rights licensed to ACM.",

year = "2022",

month = jul,

day = "31",

doi = "10.1145/3514241",

language = "English",

volume = "23",

pages = "1--29",

journal = "ACM Transactions on Computational Logic",

issn = "1529-3785",

publisher = "Association for Computing Machinery (ACM)",

number = "3",

}

TY - JOUR

T1 - Modalities and Parametric Adjoints

AU - Gratzer, Daniel

AU - Cavallo, Evan

AU - Kavvos, G. A.

AU - Guatto, Adrien

AU - Birkedal, Lars

N1 - Funding Information: The first, third, and fifth authors were supported in part by a Villum Investigator grant (no. 25804), Center for Basic Research in Program Verification (CPV), from the VILLUM Foundation. The second author was supported in part by the Knut and Alice Wallenberg foundation (no. 2020.0266) and the Air Force Office of Scientific Research under MURI grants FA9550-15-1-0053 and FA9550-19-1-0216. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of any sponsoring institution, the U.S. government, or any other entity. Authors’ addresses: D. Gratzer and L. Birkedal, Aarhus University, Aabogade 34, Aarhus, Denmark, 8200; emails: {gratzer, birkedal}@cs.au.dk; E. Cavallo, Stockholm University, SE-106 91, Stockholm, Sweden; email: [email protected]; G. A. Kavvos, University of Bristol, Merchant Venturers Building, Bristol, United Kingdom, BS8 1UB; email: alex.kavvos @bristol.ac.uk; A. Guatto, Université de Paris, CNRS, IRIF, F-75006, Paris, France; email: [email protected]. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]. © 2022 Copyright held by the owner/author(s). Publication rights licensed to ACM. 1529-3785/2022/04-ART18 $15.00 https://doi.org/10.1145/3514241 Publisher Copyright: © 2022 Copyright held by the owner/author(s). Publication rights licensed to ACM.

PY - 2022/7/31

Y1 - 2022/7/31

N2 - 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.

AB - 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.

KW - modal logic

KW - category theory

KW - type theory

U2 - 10.1145/3514241

DO - 10.1145/3514241

M3 - Article (Academic Journal)

SN - 1529-3785

VL - 23

SP - 1

EP - 29

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

IS - 3

M1 - 18

ER -

Modalities and Parametric Adjoints

Abstract

Bibliographical note

Research Groups and Themes

Keywords

Access to Document

Handle.net

Fingerprint

Cite this