Modal dependent type theory and dependent right adjoints

DOI10.1017/S0960129519000197MaRDI QIDQ5220184zbMATHWikidataFDO

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)

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

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)

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.

Recommendations

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

Cites work

• scientific article; zbMATH DE number 4191621 (Why is no real title available?)
• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 699435 (Why is no real title available?)
• scientific article; zbMATH DE number 2079044 (Why is no real title available?)
• scientific article; zbMATH DE number 6816943 (Why is no real title available?)
• scientific article; zbMATH DE number 1840601 (Why is no real title available?)
• scientific article; zbMATH DE number 7204444 (Why is no real title available?)
• scientific article; zbMATH DE number 7297837 (Why is no real title available?)
• scientific article; zbMATH DE number 3218799 (Why is no real title available?)
• scientific article; zbMATH DE number 970633 (Why is no real title available?)
• scientific article; zbMATH DE number 3076631 (Why is no real title available?)
• A C-system defined by a universe category
• A dependent type theory with abstractable names
• A modal analysis of staged computation
• A type theory for productive coprogramming via guarded recursion
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Cubical type theory: a constructive interpretation of the univalence axiom
• Denotational semantics for guarded dependent type theory
• Fibrational modal type theory
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Fitch-style modal lambda calculi
• Guarded cubical type theory
• Guarded dependent type theory with coinductive types
• Integrating linear and dependent types
• Intensional type theory with guarded recursive types qua fixed points on universes
• Internal type theory
• Internal universes in models of homotopy type theory
• Modalities in homotopy type theory
• Nominal sets. Names and symmetry in computer science
• On an intuitionistic modal logic
• Productive coprogramming with guarded recursion
• Programming and reasoning with guarded recursion for coinductive types
• Propositions as [Types]
• The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
• The clocks are ticking: no more delays!: Reduction semantics for type theory with guarded recursion
• The clocks they are adjunctions. Denotational semantics for clocked type theory
• The homotopy theory of type theories
• The local universes model: an overlooked coherence construction for dependent type theories

Cited in

(17)

• Adjoint logic with a 2-category of modes
• A general framework for the semantics of type theory
• Temporal refinements for guarded recursive types
• Modal FRP for all: Functional reactive programming without space leaks in Haskell
• When programs have to watch paint dry
• scientific article; zbMATH DE number 7561492 (Why is no real title available?)
• Normalization by evaluation for modal dependent type theory
• scientific article; zbMATH DE number 7288622 (Why is no real title available?)
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• Normalization for multimodal type theory
• Multimodal dependent type theory
• Transpension: the right adjoint to the Pi-type
• Multimodal dependent type theory
• scientific article; zbMATH DE number 7779294 (Why is no real title available?)
• Fibrational modal type theory
• UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC
• A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types

Describes a project that uses

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)