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

      Better Late Than Never: A Fully Abstract Semantics for Classical Processes

      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 present Hypersequent Classical Processes (HCP), a revised interpretation of the "Proofs as Processes" correspondence between linear logic and the {\pi}-calculus initially proposed by Abramsky [1994], and later developed by Bellin and Scott [1994], Caires and Pfenning [2010], and Wadler [2014], among others. HCP mends the discrepancies between linear logic and the syntax and observable semantics of parallel composition in the {\pi}-calculus, by conservatively extending linear logic to hyperenvironments (collections of environments, inspired by the hypersequents by Avron [1991]). Separation of environments in hyperenvironments is internalised by \(\otimes\) and corresponds to parallel process behaviour. Thanks to this property, for the first time we are able to extract a labelled transition system (lts) semantics from proof rewritings. Leveraging the information on parallelism at the level of types, we obtain a logical reconstruction of the delayed actions that Merro and Sangiorgi [2004] formulated to model non-blocking I/O in the {\pi}-calculus. We define a denotational semantics for processes based on Brzozowski derivatives, and uncover that non-interference in HCP corresponds to Fubini's theorem of double antiderivation. Having an lts allows us to validate HCP using the standard toolbox of behavioural theory. We instantiate bisimilarity and barbed congruence for HCP, and obtain a full abstraction result: bisimilarity, denotational equivalence, and barbed congruence coincide.

          Related collections

          Most cited references21

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

          Linear logic

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

            Derivatives of Regular Expressions

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

              Session Types as Intuitionistic Linear Propositions

                Bookmark

                Author and article information

                Journal
                06 November 2018
                Article
                1811.02209
                6c5caa0e-b20c-43d6-8703-e35fd63d67cd

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

                History
                Custom metadata
                cs.LO

                Theoretical computer science
                Theoretical computer science

                Comments

                Comment on this article