Dual-Context Calculi for Modal Logic

G. A. Kavvos

doi:10.1109/LICS.2017.8005089

Dual-Context Calculi for Modal Logic

G. A. Kavvos

Research output: Chapter in Book/Report/Conference proceeding › Conference Contribution (Conference Proceeding)

21 Citations (Scopus)

377 Downloads (Pure)

Abstract

We show how to derive natural deduction systems for the necessity fragment of various constructive modal logics by exploiting a pattern found in sequent calculi. The resulting systems are dual-context systems, in the style pioneered by Girard, Barber, Plotkin, Pfenning, Davies, and others. This amounts to a full extension of the Curry-Howard-Lambek correspondence to the necessity fragments of a constructive variant of the modal logics K, K4, GL, T, and S4. We investigate the metatheory of these calculi, as well as their categorical semantics. Finally, we speculate on their computational interpretation

Original language	English
Title of host publication	2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
Pages	1-12
Number of pages	12
Volume	August 2017
ISBN (Electronic)	9781509030187
ISBN (Print)	9781509030194
DOIs	https://doi.org/10.1109/LICS.2017.8005089
Publication status	Published - 18 Aug 2017
Event	Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017) - Reykjavik University, Reykjavik, Iceland Duration: 20 Jun 2017 → 23 Jun 2017 Conference number: 2017 http://lics.siglog.org/lics17/

Publication series

Name
ISSN (Electronic)	1043-6871

Conference

Conference	Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)
Abbreviated title	LICS
Country/Territory	Iceland
City	Reykjavik
Period	20/06/17 → 23/06/17
Internet address	http://lics.siglog.org/lics17/

Research Groups and Themes

Programming Languages

Keywords

modal logic
comonads
semantics
proof theory
Curry-Howard
lambda calculus

Access to Document

10.1109/LICS.2017.8005089

Full-text PDF (author accepted manuscript)
This is the author accepted manuscript (AAM). The final published version (version of record) is available online via IEEE at https://ieeexplore.ieee.org/document/8005089. Please refer to any applicable terms of use of the publisher.
Accepted author manuscript, 372 KB

https://arxiv.org/abs/1602.04860v4

Handle.net

Persistent link

21 Citations
1 Article (Academic Journal)

Dual-Context Calculi for Modal Logic
Kavvos, G. A., 19 Aug 2020, In: Logical Methods in Computer Science (LMCS). 16, 3, p. 10:1–10:66 66 p.
Research output: Contribution to journal › Article (Academic Journal) › peer-review

Open Access
File
12 Citations (Scopus)

237 Downloads (Pure)

Dr Alex Kavvos
- alex.kavvosbristol.acuk
- School of Computer Science - Associate Professor in Logic and Programming Languages
Person: Academic

Cite this

@inproceedings{0dde624e3f6c483eb115462f0d404062,

title = "Dual-Context Calculi for Modal Logic",

abstract = "We show how to derive natural deduction systems for the necessity fragment of various constructive modal logics by exploiting a pattern found in sequent calculi. The resulting systems are dual-context systems, in the style pioneered by Girard, Barber, Plotkin, Pfenning, Davies, and others. This amounts to a full extension of the Curry-Howard-Lambek correspondence to the necessity fragments of a constructive variant of the modal logics K, K4, GL, T, and S4. We investigate the metatheory of these calculi, as well as their categorical semantics. Finally, we speculate on their computational interpretation",

keywords = "modal logic, comonads, semantics, proof theory, Curry-Howard, lambda calculus",

author = "Kavvos, \{G. A.\}",

year = "2017",

month = aug,

day = "18",

doi = "10.1109/LICS.2017.8005089",

language = "English",

isbn = "9781509030194",

volume = "August 2017",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

pages = "1--12",

booktitle = "2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)",

address = "United States",

note = "Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), LICS ; Conference date: 20-06-2017 Through 23-06-2017",

url = "http://lics.siglog.org/lics17/",

}

Kavvos, GA 2017, Dual-Context Calculi for Modal Logic. in 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). vol. August 2017, Institute of Electrical and Electronics Engineers (IEEE), pp. 1-12, Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), Reykjavik, Iceland, 20/06/17. https://doi.org/10.1109/LICS.2017.8005089

TY - GEN

T1 - Dual-Context Calculi for Modal Logic

AU - Kavvos, G. A.

N1 - Conference code: 2017

PY - 2017/8/18

Y1 - 2017/8/18

N2 - We show how to derive natural deduction systems for the necessity fragment of various constructive modal logics by exploiting a pattern found in sequent calculi. The resulting systems are dual-context systems, in the style pioneered by Girard, Barber, Plotkin, Pfenning, Davies, and others. This amounts to a full extension of the Curry-Howard-Lambek correspondence to the necessity fragments of a constructive variant of the modal logics K, K4, GL, T, and S4. We investigate the metatheory of these calculi, as well as their categorical semantics. Finally, we speculate on their computational interpretation

AB - We show how to derive natural deduction systems for the necessity fragment of various constructive modal logics by exploiting a pattern found in sequent calculi. The resulting systems are dual-context systems, in the style pioneered by Girard, Barber, Plotkin, Pfenning, Davies, and others. This amounts to a full extension of the Curry-Howard-Lambek correspondence to the necessity fragments of a constructive variant of the modal logics K, K4, GL, T, and S4. We investigate the metatheory of these calculi, as well as their categorical semantics. Finally, we speculate on their computational interpretation

KW - modal logic

KW - comonads

KW - semantics

KW - proof theory

KW - Curry-Howard

KW - lambda calculus

U2 - 10.1109/LICS.2017.8005089

DO - 10.1109/LICS.2017.8005089

M3 - Conference Contribution (Conference Proceeding)

SN - 9781509030194

VL - August 2017

SP - 1

EP - 12

BT - 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

PB - Institute of Electrical and Electronics Engineers (IEEE)

T2 - Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)

Y2 - 20 June 2017 through 23 June 2017

ER -

Dual-Context Calculi for Modal Logic

Abstract

Publication series

Conference

Research Groups and Themes

Keywords

Access to Document

Handle.net

Fingerprint

Research output

Dual-Context Calculi for Modal Logic

Profiles

Dr Alex Kavvos

Cite this