Under Lock and Key: A Proof System for a Multimodal Logic

TY - JOUR

T1 - Under Lock and Key

T2 - A Proof System for a Multimodal Logic

AU - Kavvos, G. A.

AU - Gratzer, Daniel

PY - 2023/6/20

Y1 - 2023/6/20

N2 - 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.

AB - 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.

KW - 03-02 03B40 03B45 03B70 03F07

UR - http://www.scopus.com/inward/record.url?scp=85153956495&partnerID=8YFLogxK

U2 - 10.1017/bsl.2023.14

DO - 10.1017/bsl.2023.14

M3 - Journal article

SN - 1079-8986

VL - 29

SP - 264

EP - 293

JO - Bulletin of Symbolic Logic

JF - Bulletin of Symbolic Logic

IS - 2

ER -