Processing math: 100%
17
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Taking Linear Logic Apart

      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

          Process calculi based on logic, such as πDILL and CP, provide a foundation for deadlock-free concurrent programming. However, in previous work, there is a mismatch between the rules for constructing proofs and the term constructors of the π-calculus: the fundamental operator for parallel composition does not correspond to any rule of linear logic. Kokke et al. (2019) introduced Hypersequent Classical Processes (HCP), which addresses this mismatch using hypersequents (collections of sequents) to register parallelism in the typing judgements. However, the step from CP to HCP is a big one. As of yet, HCP does not have reduction semantics, and the addition of delayed actions means that CP processes interpreted as HCP processes do not behave as they would in CP. We introduce HCP-, a variant of HCP with reduction semantics and without delayed actions. We prove progress, preservation, and termination, and show that HCP- supports the same communication protocols as CP.

          Related collections

          Most cited references17

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

          A calculus of mobile processes, I

            Bookmark
            • Record: found
            • Abstract: not found
            • Book Chapter: not found

            Language primitives and type discipline for structured communication-based programming

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

              A calculus of mobile processes, II

                Bookmark

                Author and article information

                Journal
                15 April 2019
                Article
                10.4204/EPTCS.292.5
                1904.06848
                070a6fc6-29f5-470b-aa3b-a399f27d2123

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                EPTCS 292, 2019, pp. 90-103
                In Proceedings Linearity-TLLA 2018, arXiv:1904.06159
                cs.LO cs.PL
                EPTCS

                Theoretical computer science,Programming languages
                Theoretical computer science, Programming languages

                Comments

                Comment on this article

                scite_
                9
                0
                12
                0
                Smart Citations
                9
                0
                12
                0
                Citing PublicationsSupportingMentioningContrasting
                View Citations

                See how this article has been cited at scite.ai

                scite shows how a scientific paper has been cited by providing the context of the citation, a classification describing whether it supports, mentions, or contrasts the cited claim, and a label indicating in which section the citation was made.

                Similar content75

                Most referenced authors3,283