Modal dependent type theory and dependent right adjoints

DOI10.1017/S0960129519000197zbMATH Open1479.03011arXiv1804.05236WikidataQ126579053 ScholiaQ126579053MaRDI QIDQ5220184FDOQ5220184

Authors: Ranald A. Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, Bas Spitters, Lars Birkedal 

Publication date: 11 March 2020

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

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 finite limit category with an adjunction of endofunctors gives rise to a CwDRA via the local universe construction. For the syntax, we introduce a dependently typed extension of Fitch-style modal lambda-calculus, show that it can be interpreted in any CwDRA, and build a term model. We extend the syntax and semantics with universes.

Full work available at URL: https://arxiv.org/abs/1804.05236

Recommendations

• Modalities and Parametric Adjoints
• Fibrational modal type theory
• Multimodal dependent type theory
• Multimodal dependent type theory
• Modalities in homotopy type theory

zbMATH Keywords

category theorymodal logicdependent type theory

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Combinatory logic and lambda calculus (03B40) Adjoint functors (universal constructions, reflective subcategories, Kan extensions, etc.) (18A40) Type theory (03B38)

Cites Work

• On an intuitionistic modal logic
• Nominal sets. Names and symmetry in computer science
• Title not available (Why is that?)
• A modal analysis of staged computation
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Internal type theory
• Title not available (Why is that?)
• The Local Universes Model
• A dependent type theory with abstractable names
• Title not available (Why is that?)
• Title not available (Why is that?)
• The homotopy theory of type theories
• Title not available (Why is that?)
• Fitch-style modal lambda calculi
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Guarded Dependent Type Theory with Coinductive Types
• Programming and Reasoning with Guarded Recursion for Coinductive Types
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• A type theory for productive coprogramming via guarded recursion
• Productive coprogramming with guarded recursion
• Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Modalities in homotopy type theory
• Fibrational modal type theory
• Integrating linear and dependent types
• Propositions as [Types]
• A C-system defined by a universe category
• Title not available (Why is that?)
• Guarded cubical type theory
• Denotational semantics for guarded dependent type theory
• Title not available (Why is that?)
• The biequivalence of locally cartesian closed categories and Martin-Löf type theories
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (13)

• When programs have to watch paint dry
• Transpension: the right adjoint to the Pi-type
• Title not available (Why is that?)
• A general framework for the semantics of type theory
• Temporal refinements for guarded recursive types
• UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC
• Title not available (Why is that?)
• Title not available (Why is that?)
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• Normalization for multimodal type theory
• Normalization by evaluation for modal dependent type theory
• A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types
• Modal FRP for all: Functional reactive programming without space leaks in Haskell

Uses Software

• cubicaltt
• MiniML

This page was built for publication: Modal dependent type theory and dependent right adjoints

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5220184)