Taking Linear Logic Apart

Wen Kokke; Fabrizio Montesi; Marco Peressotti

doi:10.4204/EPTCS.292.5

Taking Linear Logic Apart

Wen Kokke, Fabrizio Montesi, Marco Peressotti

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

66 Downloads (Pure)

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. [12] 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.

Original language	English
Title of host publication	Proceedings of the Joint International Workshop on Linearity Trends in linear Logic and Applications
Editors	Thomas Ehrhard, Maribel Fernández, Valeria de Paiva, Lorenzo Tortora de Falco
Volume	292
Publisher	Open Publishing Association
Publication date	15. Apr 2019
Pages	90-103
DOIs	https://doi.org/10.4204/EPTCS.292.5
Publication status	Published - 15. Apr 2019
Event	2018 Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity-TLLA 2018 - Oxford, United Kingdom Duration: 7. Jul 2018 → 8. Jul 2018

Conference

Conference	2018 Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity-TLLA 2018
Country/Territory	United Kingdom
City	Oxford
Period	07/07/2018 → 08/07/2018

Series	Electronic Proceedings in Theoretical Computer Science, EPTCS
Volume	292
ISSN	2075-2180

Keywords

Curry-Howard correspondence
Deadlock-freedom
Logic
Linear logic
Process calculi
Programming Languages
Formal methods

Documents & Links

10.4204/EPTCS.292.5

Taking Linear Logic ApartFinal published version, 166 KBLicence: CC BY

Cite this

Kokke, W., Montesi, F., & Peressotti, M. (2019). Taking Linear Logic Apart. In T. Ehrhard, M. Fernández, V. de Paiva, & L. Tortora de Falco (Eds.), Proceedings of the Joint International Workshop on Linearity Trends in linear Logic and Applications (Vol. 292, pp. 90-103). Open Publishing Association. Electronic Proceedings in Theoretical Computer Science, EPTCS Vol. 292 https://doi.org/10.4204/EPTCS.292.5

Kokke, Wen ; Montesi, Fabrizio ; Peressotti, Marco. / Taking Linear Logic Apart. Proceedings of the Joint International Workshop on Linearity Trends in linear Logic and Applications. editor / Thomas Ehrhard ; Maribel Fernández ; Valeria de Paiva ; Lorenzo Tortora de Falco. Vol. 292 Open Publishing Association, 2019. pp. 90-103 (Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol. 292).

@inproceedings{c7f9d7bc56d1457d83a2d0f7c46250a9,

title = "Taking Linear Logic Apart",

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. [12] 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. ",

keywords = "Curry-Howard correspondence, Deadlock-freedom, Logic, Linear logic, Process calculi, Programming Languages, Formal methods",

author = "Wen Kokke and Fabrizio Montesi and Marco Peressotti",

year = "2019",

month = apr,

day = "15",

doi = "10.4204/EPTCS.292.5",

language = "English",

volume = "292",

series = "Electronic Proceedings in Theoretical Computer Science, EPTCS",

publisher = "Open Publishing Association",

pages = "90--103",

editor = "Thomas Ehrhard and Maribel Fern{\'a}ndez and {de Paiva}, Valeria and {Tortora de Falco}, Lorenzo",

booktitle = "Proceedings of the Joint International Workshop on Linearity Trends in linear Logic and Applications",

note = "2018 Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity-TLLA 2018 ; Conference date: 07-07-2018 Through 08-07-2018",

}

Kokke, W, Montesi, F & Peressotti, M 2019, Taking Linear Logic Apart. in T Ehrhard, M Fernández, V de Paiva & L Tortora de Falco (eds), Proceedings of the Joint International Workshop on Linearity Trends in linear Logic and Applications. vol. 292, Open Publishing Association, Electronic Proceedings in Theoretical Computer Science, EPTCS, vol. 292, pp. 90-103, 2018 Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity-TLLA 2018, Oxford, United Kingdom, 07/07/2018. https://doi.org/10.4204/EPTCS.292.5

Taking Linear Logic Apart. / Kokke, Wen; Montesi, Fabrizio ; Peressotti, Marco.

Proceedings of the Joint International Workshop on Linearity Trends in linear Logic and Applications. ed. / Thomas Ehrhard; Maribel Fernández; Valeria de Paiva; Lorenzo Tortora de Falco. Vol. 292 Open Publishing Association, 2019. p. 90-103 (Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol. 292).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Taking Linear Logic Apart

AU - Kokke, Wen

AU - Montesi, Fabrizio

AU - Peressotti, Marco

PY - 2019/4/15

Y1 - 2019/4/15

N2 - 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. [12] 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.

AB - 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. [12] 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.

KW - Curry-Howard correspondence

KW - Deadlock-freedom

KW - Logic

KW - Linear logic

KW - Process calculi

KW - Programming Languages

KW - Formal methods

U2 - 10.4204/EPTCS.292.5

DO - 10.4204/EPTCS.292.5

M3 - Article in proceedings

VL - 292

T3 - Electronic Proceedings in Theoretical Computer Science, EPTCS

SP - 90

EP - 103

BT - Proceedings of the Joint International Workshop on Linearity Trends in linear Logic and Applications

A2 - Ehrhard, Thomas

A2 - Fernández, Maribel

A2 - de Paiva, Valeria

A2 - Tortora de Falco, Lorenzo

PB - Open Publishing Association

T2 - 2018 Joint International Workshop on Linearity and Trends in Linear Logic and Applications, Linearity-TLLA 2018

Y2 - 7 July 2018 through 8 July 2018

ER -

Kokke W, Montesi F , Peressotti M. Taking Linear Logic Apart. In Ehrhard T, Fernández M, de Paiva V, Tortora de Falco L, editors, Proceedings of the Joint International Workshop on Linearity Trends in linear Logic and Applications. Vol. 292. Open Publishing Association. 2019. p. 90-103. (Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol. 292). https://doi.org/10.4204/EPTCS.292.5

Taking Linear Logic Apart

Abstract

Conference

Keywords

Documents & Links

Other files and links

Fingerprint

Better Late Than Never: A Fully-abstract Semantics for Classical Processes

Cite this

Taking Linear Logic Apart

Abstract

Conference

Keywords

Documents & Links

Other files and links

Fingerprint

Related Research Output

Better Late Than Never: A Fully-abstract Semantics for Classical Processes

Cite this