5
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      A Linear-logical Reconstruction of Intuitionistic Modal Logic S4

      Preprint

      ,

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          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.

          Related collections

          Most cited references 18

          • Record: found
          • Abstract: not found
          • Article: not found

          Linear logic

            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            Decision problems for propositional linear logic

              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              MetaML and multi-stage programming with explicit annotations

                Bookmark

                Author and article information

                Journal
                23 April 2019
                Article
                1904.10605

                http://creativecommons.org/licenses/by/4.0/

                Custom metadata
                Author copy of a paper accepted for FSCD 2019
                cs.LO

                Theoretical computer science

                Comments

                Comment on this article