Taking Linear Logic Apart
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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2019-04-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1904.06848v1 |
| _version_ | 1818033790564433920 |
|---|---|
| author | Wen Kokke Fabrizio Montesi Marco Peressotti |
| author_facet | Wen Kokke Fabrizio Montesi Marco Peressotti |
| author_sort | Wen Kokke |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-10T06:28:52Z |
| format | Article |
| id | doaj.art-2820cc5c92e6484c8c9e2597bf28bbfd |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-10T06:28:52Z |
| publishDate | 2019-04-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-2820cc5c92e6484c8c9e2597bf28bbfd2022-12-22T01:59:07ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802019-04-01292Proc. Linearity-TLLA 20189010310.4204/EPTCS.292.5:5Taking Linear Logic ApartWen Kokke0Fabrizio Montesi1Marco Peressotti2 University of Edinburgh University of Southern Denmark University of Southern Denmark 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.http://arxiv.org/pdf/1904.06848v1 |
| spellingShingle | Wen Kokke Fabrizio Montesi Marco Peressotti Taking Linear Logic Apart Electronic Proceedings in Theoretical Computer Science |
| title | Taking Linear Logic Apart |
| title_full | Taking Linear Logic Apart |
| title_fullStr | Taking Linear Logic Apart |
| title_full_unstemmed | Taking Linear Logic Apart |
| title_short | Taking Linear Logic Apart |
| title_sort | taking linear logic apart |
| url | http://arxiv.org/pdf/1904.06848v1 |
| work_keys_str_mv | AT wenkokke takinglinearlogicapart AT fabriziomontesi takinglinearlogicapart AT marcoperessotti takinglinearlogicapart |