Multimodal dependent type theory

DOI10.1145/3373718.3394736zbMATH Open1498.03029OpenAlexW3030119148MaRDI QIDQ5145658FDOQ5145658

Authors: Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal 

Publication date: 21 January 2021

Published in: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/3373718.3394736

Recommendations

• Multimodal dependent type theory
• Modalities and Parametric Adjoints
• Modal dependent type theory and dependent right adjoints
• Guarded dependent type theory with coinductive types
• Fibrational modal type theory

zbMATH Keywords

categorical semanticsdependent typesgluingguarded recursionmodal types

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Type theory (03B38)

Cited In (13)

• Transpension: the right adjoint to the Pi-type
• Title not available (Why is that?)
• Fibrational modal type theory
• Graded modal dependent 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?)
• 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
• Modal dependent type theory and dependent right adjoints
• Multimodal dependent type theory
• Constructing unprejudiced extensional type theories with choices via modalities

This page was built for publication: Multimodal dependent type theory

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