UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC
G. A. Kavvos, Daniel Gratzer · Bulletin of Symbolic Logic · 2023
Abstract We present a proof system for a multimode and multimodal logic, which is based on our previous work on modal Martin-Löf 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.