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

G. A. Kavvos; Daniel Gratzer

doi:10.1017/bsl.2023.14

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

G. A. Kavvos
, Daniel Gratzer

Research output: Contribution to journal › Article (Academic Journal) › peer-review

3 Citations (Scopus)

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.

Original language	English
Pages (from-to)	264-293
Number of pages	30
Journal	Bulletin of Symbolic Logic
Volume	29
Issue number	2
Early online date	20 Apr 2023
DOIs	https://doi.org/10.1017/bsl.2023.14
Publication status	Published - 1 Jun 2023

Bibliographical note

Publisher Copyright:
© The Author(s), 2023. Published by Cambridge University Press on behalf of The Association for Symbolic Logic.

Research Groups and Themes

Programming Languages

Access to Document

10.1017/bsl.2023.14Licence: CC BY

Handle.net

Persistent link

Cite this

@article{adb418d679ed4fe898283884f72d0afa,

title = "Under Lock and Key: A Proof System for a Multimodal Logic",

abstract = "We present a proof system for a multimode and multimodal logic, which is based on our previous work on modal Martin-L{\"o}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. ",

author = "Kavvos, \{G. A.\} and Daniel Gratzer",

note = "Publisher Copyright: {\textcopyright} The Author(s), 2023. Published by Cambridge University Press on behalf of The Association for Symbolic Logic.",

year = "2023",

month = jun,

day = "1",

doi = "10.1017/bsl.2023.14",

language = "English",

volume = "29",

pages = "264--293",

journal = "Bulletin of Symbolic Logic",

issn = "1079-8986",

publisher = "Cambridge University Press",

number = "2",

}

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/1

Y1 - 2023/6/1

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.

U2 - 10.1017/bsl.2023.14

DO - 10.1017/bsl.2023.14

M3 - Article (Academic Journal)

SN - 1079-8986

VL - 29

SP - 264

EP - 293

JO - Bulletin of Symbolic Logic

JF - Bulletin of Symbolic Logic

IS - 2

ER -

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

Abstract

Bibliographical note

Research Groups and Themes

Access to Document

Handle.net

Fingerprint

Cite this