Taking Linear Logic Apart

All publications

Taking Linear Logic Apart

Wen Kokke, Fabrizio Montesi, Marco Peressotti [2018].
In proceedings of Linearity-TLLA@FLoC 2018, pp. 90-103.

Abstract

Process calculi based on logic, such as $\pi$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 $\pi$-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.

Links

Additional notes

None

Cite (BibTeX)

Click to expand

@inproceedings{DBLP:journals/corr/abs-1904-06848,
  author       = {Wen Kokke and
                  Fabrizio Montesi and
                  Marco Peressotti},
  editor       = {Thomas Ehrhard and
                  Maribel Fern{\'{a}}ndez and
                  Valeria de Paiva and
                  Lorenzo Tortora de Falco},
  title        = {Taking Linear Logic Apart},
  booktitle    = {Proceedings Joint International Workshop on Linearity {\&} Trends
                  in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, Oxford,
                  UK, 7-8 July 2018},
  series       = {{EPTCS}},
  volume       = {292},
  pages        = {90--103},
  year         = {2018},
  url          = {https://doi.org/10.4204/EPTCS.292.5},
  doi          = {10.4204/EPTCS.292.5},
  timestamp    = {Sat, 19 Oct 2019 19:22:56 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-1904-06848.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

A PDF is available (possibly a preprint):