Two-dimensional Kripke Semantics I: Presheaves

G. A. Kavvos

doi:10.4230/LIPIcs.FSCD.2024.14

Two-dimensional Kripke Semantics I: Presheaves

G. A. Kavvos

School of Computer Science

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

5 Citations (Scopus)

422 Downloads (Pure)

Abstract

The study of modal logic has witnessed tremendous development following the introduction of Kripke semantics. However, recent developments in programming languages and type theory have led to a second way of studying modalities, namely through their categorical semantics. We show how the two correspond.

Original language	English
Title of host publication	9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Editors	Jakob Rehof
Publisher	Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
Number of pages	23
Volume	299
ISBN (Electronic)	9783959773232
ISBN (Print)	9783959773232
DOIs	https://doi.org/10.4230/LIPIcs.FSCD.2024.14
Publication status	Published - 5 Jul 2024
Event	9th International Conference on Formal Structures for Computation and Deduction - Talinn, Estonia Duration: 10 Jul 2024 → 13 Jul 2024 https://cs.ioc.ee/fscd24/

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Volume	299
ISSN (Print)	1868-8969

Conference

Conference	9th International Conference on Formal Structures for Computation and Deduction
Abbreviated title	FSCD 2024
Country/Territory	Estonia
City	Talinn
Period	10/07/24 → 13/07/24
Internet address	https://cs.ioc.ee/fscd24/

Bibliographical note

Publisher Copyright:
© Georgios Alexandros Kavvos.

Research Groups and Themes

Programming Languages

Keywords

logic
modal logic
category theory
duality
semantics
profunctors

Access to Document

10.4230/LIPIcs.FSCD.2024.14Licence: CC BY

Full-text PDF (accepted manuscript)
This is the accepted author manuscript (AAM) of the article which has been made Open Access under the University of Bristol's Scholarly Works Policy. The final published version (Version of Record) can be found on the publisher's website. The copyright of any third-party content, such as images, remains with the copyright holder.
Accepted author manuscript, 599 KBLicence: CC BY

Handle.net

Persistent link

Cite this

Kavvos, G. A. (2024). Two-dimensional Kripke Semantics I: Presheaves. In J. Rehof (Ed.), 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024) (Vol. 299). Article 14 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 299). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. https://doi.org/10.4230/LIPIcs.FSCD.2024.14

@inproceedings{dcd2d34070594e6a921921b975321756,

title = "Two-dimensional Kripke Semantics I: Presheaves",

abstract = "The study of modal logic has witnessed tremendous development following the introduction of Kripke semantics. However, recent developments in programming languages and type theory have led to a second way of studying modalities, namely through their categorical semantics. We show how the two correspond. ",

keywords = "logic, modal logic, category theory, duality, semantics, profunctors",

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

note = "Publisher Copyright: {\textcopyright} Georgios Alexandros Kavvos.; 9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024 ; Conference date: 10-07-2024 Through 13-07-2024",

year = "2024",

month = jul,

day = "5",

doi = "10.4230/LIPIcs.FSCD.2024.14",

language = "English",

isbn = "9783959773232",

volume = "299",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany",

editor = "Jakob Rehof",

booktitle = "9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)",

url = "https://cs.ioc.ee/fscd24/",

}

Kavvos, GA 2024, Two-dimensional Kripke Semantics I: Presheaves. in J Rehof (ed.), 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). vol. 299, 14, Leibniz International Proceedings in Informatics, LIPIcs, vol. 299, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 9th International Conference on Formal Structures for Computation and Deduction, Talinn, Estonia, 10/07/24. https://doi.org/10.4230/LIPIcs.FSCD.2024.14

Two-dimensional Kripke Semantics I: Presheaves. / Kavvos, G. A.
9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). ed. / Jakob Rehof. Vol. 299 Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2024. 14 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 299).

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

TY - GEN

T1 - Two-dimensional Kripke Semantics I

T2 - 9th International Conference on Formal Structures for Computation and Deduction

AU - Kavvos, G. A.

PY - 2024/7/5

Y1 - 2024/7/5

N2 - The study of modal logic has witnessed tremendous development following the introduction of Kripke semantics. However, recent developments in programming languages and type theory have led to a second way of studying modalities, namely through their categorical semantics. We show how the two correspond.

AB - The study of modal logic has witnessed tremendous development following the introduction of Kripke semantics. However, recent developments in programming languages and type theory have led to a second way of studying modalities, namely through their categorical semantics. We show how the two correspond.

KW - logic

KW - modal logic

KW - category theory

KW - duality

KW - semantics

KW - profunctors

UR - https://fscd-conference.org/

U2 - 10.4230/LIPIcs.FSCD.2024.14

DO - 10.4230/LIPIcs.FSCD.2024.14

M3 - Conference Contribution (Conference Proceeding)

SN - 9783959773232

VL - 299

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

A2 - Rehof, Jakob

PB - Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany

Y2 - 10 July 2024 through 13 July 2024

ER -

Two-dimensional Kripke Semantics I: Presheaves

Abstract

Publication series

Conference

Bibliographical note

Research Groups and Themes

Keywords

Access to Document

Handle.net

Other files and links

Fingerprint

Towards Directed Model Categories

Language Embeddings for Proof Engineering

Towards Concurrent Classical Effects

Cite this

Two-dimensional Kripke Semantics I: Presheaves

Abstract

Publication series

Conference

Bibliographical note

Research Groups and Themes

Keywords

Access to Document

Handle.net

Other files and links

Fingerprint

Projects

Towards Directed Model Categories

Language Embeddings for Proof Engineering

Towards Concurrent Classical Effects

Cite this