License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2019.20
URN: urn:nbn:de:0030-drops-105271
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10527/
Go to the corresponding LIPIcs Volume Portal

Fukuda, Yosuke ; Yoshimizu, Akira

A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4

pdf-format:
LIPIcs-FSCD-2019-20.pdf (1 MB)

Abstract

We propose a modal linear logic to reformulate intuitionistic modal logic S4 (IS4) in terms of linear logic, establishing an S4-version of Girard translation from IS4 to it. While the Girard translation from intuitionistic logic to linear logic is well-known, its extension to modal logic is non-trivial since a naive combination of the S4 modality and the exponential modality causes an undesirable interaction between the two modalities. To solve the problem, we introduce an extension of intuitionistic multiplicative exponential linear logic with a modality combining the S4 modality and the exponential modality, and show that it admits a sound translation from IS4. Through the Curry-Howard correspondence we further obtain a Geometry of Interaction Machine semantics of the modal lambda-calculus by Pfenning and Davies for staged computation.

BibTeX - Entry

@InProceedings{fukuda_et_al:LIPIcs:2019:10527,
  author =	{Yosuke Fukuda and Akira Yoshimizu},
  title =	{{A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{20:1--20:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Herman Geuvers},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10527},
  URN =		{urn:nbn:de:0030-drops-105271},
  doi =		{10.4230/LIPIcs.FSCD.2019.20},
  annote =	{Keywords: linear logic, modal logic, Girard translation, Curry-Howard correspondence, geometry of interaction, staged computation}
}

Keywords: linear logic, modal logic, Girard translation, Curry-Howard correspondence, geometry of interaction, staged computation
Collection: 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Issue Date: 2019
Date of publication: 18.06.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI