Multimodal dependent type theory

DOI10.1145/3373718.3394736MaRDI QIDQ5145658zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

categorical semanticsdependent typesgluingguarded recursionmodal types

Mathematics Subject Classification ID

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

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

Cited in

(21)

• Fibrational modal type theory
• Graded modal dependent type theory
• Temporal refinements for guarded recursive types
• scientific article; zbMATH DE number 7288622 (Why is no real title available?)
• Multimodal dependent type theory
• Modal dependent type theory and dependent right adjoints
• Normalization by evaluation for modal dependent type theory
• scientific article; zbMATH DE number 7779294 (Why is no real title available?)
• UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC
• Constructing unprejudiced extensional type theories with choices via modalities
• Transpension: the right adjoint to the Pi-type
• Normalization for multimodal type theory
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• Two-dimensional Kripke semantics. II: Stability and completeness
• Normalization for multimodal type theory
• What monads can and cannot do with a bit of extra time
• What monads can and cannot do with a few extra pages
• Two-dimensional Kripke semantics i: presheaves
• Unifying cubical and multimodal type theory
• Strict universes for Grothendieck topoi
• Synthetic 1-categories in directed type theory

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)