Modal dependent type theory and dependent right adjoints

Lars Birkedal; Ranald Clouston; Bassel Mannaa; Rasmus Ejlers Møgelberg; Andrew M. Pitts; Bas Spitters

doi:10.1017/S0960129519000197

Modal dependent type theory and dependent right adjoints

Lars Birkedal, Ranald Clouston, Bassel Mannaa^*, Rasmus Ejlers Møgelberg, Andrew M. Pitts, Bas Spitters

^*Corresponding author for this work

Department of Computer Science

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

23 Citations (Scopus)

Abstract

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 modal dependent type theory: 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 dependent right adjoint (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 λ-calculus, show that it can be interpreted in any CwDRA, and build a term model. We extend the syntax and semantics with universes.

Original language	English
Journal	Mathematical Structures in Computer Science
Volume	30
Issue	2
Pages (from-to)	118-138
Number of pages	21
ISSN	0960-1295
DOIs	https://doi.org/10.1017/S0960129519000197
Publication status	Published - Feb 2020

Keywords

category theory
Dependent type theory
modal logic

Access to Document

10.1017/S0960129519000197

https://arxiv.org/pdf/1804.05236.pdf

Cite this

@article{6d47a5749aaa4c698485c8a490847236,

title = "Modal dependent type theory and dependent right adjoints",

abstract = "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 modal dependent type theory: 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 dependent right adjoint (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 λ-calculus, show that it can be interpreted in any CwDRA, and build a term model. We extend the syntax and semantics with universes.",

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

author = "Lars Birkedal and Ranald Clouston and Bassel Mannaa and {Ejlers M{\o}gelberg}, Rasmus and Pitts, {Andrew M.} and Bas Spitters",

year = "2020",

month = feb,

doi = "10.1017/S0960129519000197",

language = "English",

volume = "30",

pages = "118--138",

journal = "Mathematical Structures in Computer Science",

issn = "0960-1295",

publisher = "Cambridge University Press",

number = "2",

}

TY - JOUR

T1 - Modal dependent type theory and dependent right adjoints

AU - Birkedal, Lars

AU - Clouston, Ranald

AU - Mannaa, Bassel

AU - Ejlers Møgelberg, Rasmus

AU - Pitts, Andrew M.

AU - Spitters, Bas

PY - 2020/2

Y1 - 2020/2

N2 - 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 modal dependent type theory: 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 dependent right adjoint (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 λ-calculus, show that it can be interpreted in any CwDRA, and build a term model. We extend the syntax and semantics with universes.

AB - 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 modal dependent type theory: 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 dependent right adjoint (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 λ-calculus, show that it can be interpreted in any CwDRA, and build a term model. We extend the syntax and semantics with universes.

KW - category theory

KW - Dependent type theory

KW - modal logic

U2 - 10.1017/S0960129519000197

DO - 10.1017/S0960129519000197

M3 - Journal article

AN - SCOPUS:85076567664

SN - 0960-1295

VL - 30

SP - 118

EP - 138

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

IS - 2

ER -

Modal dependent type theory and dependent right adjoints

Abstract

Keywords

Access to Document

Fingerprint

Cite this