论文标题
在锁定和钥匙下：多模式逻辑的证明系统
Under Lock and Key: A Proof System for a Multimodal Logic
论文作者
论文摘要
我们基于我们先前关于多模式Martin-Loef类型理论的工作，为多模式逻辑提供了一个证明系统。它们之间的模式，模式和含义的规范是作为模式理论（即小型2类别）给出的。该逻辑扩展到lambda演算，建立了咖喱 - 霍尔德对应关系。
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.
