Under Lock and Key: A Proof System for a Multimodal Logic
Logic in Computer Science
2023-05-22 v2 Logic
Abstract
We present a proof system for a multimodal logic, based on our previous work on a multimodal Martin-Loef type theory. The specification of modes, modalities, and implications between them is given as a mode theory, i.e. a small 2-category. The logic is extended to a lambda calculus, establishing a Curry-Howard correspondence.
Keywords
Cite
@article{arxiv.2211.06217,
title = {Under Lock and Key: A Proof System for a Multimodal Logic},
author = {G. A. Kavvos and Daniel Gratzer},
journal= {arXiv preprint arXiv:2211.06217},
year = {2023}
}
Comments
Version of Record to appear in the Bulletin of Symbolic Logic