Modal dependent type theory and dependent right adjoints

DOI10.1017/S0960129519000197zbMath1479.03011arXiv1804.05236WikidataQ126579053 ScholiaQ126579053MaRDI QIDQ5220184

Bassel Mannaa, Bas Spitters, Rasmus Ejlers Møgelberg, Ranald Clouston, Andrew M. Pitts, 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

modal logiccategory theorydependent type theory

Mathematics Subject Classification ID

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

Related Items (10)

A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types ⋮ Normalization by evaluation for modal dependent type theory ⋮ When programs have to watch paint dry ⋮ Modal FRP for all: Functional reactive programming without space leaks in Haskell ⋮ A general framework for the semantics of type theory ⋮ UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC ⋮ Unnamed Item ⋮ Temporal refinements for guarded recursive types ⋮ Unnamed Item ⋮ Unnamed Item

Uses Software

• cubicaltt
• MiniML

Cites Work

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

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