Towards Races in Linear Logic

Kerewin Kokke; J. Garrett  Morris; Philip Wadler

doi:10.1007/978-3-030-22397-7_3

Towards Races in Linear Logic

Kerewin Kokke, J. Garrett Morris, Philip Wadler

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract / Description of output

Process calculi based in logic, such as πDILL and CP, provide a foundation for deadlock-free concurrent programming, but exclude nondeterminism and races. HCP is a reformulation of CP which addresses a fundamental shortcoming: the fundamental operator for parallel composition from the π-calculus does not correspond to any rule of linear logic, and therefore not to any term construct in CP.

We introduce HCP− _ND, which extends HCP with a novel account of nondeterminism. Our approach draws on bounded linear logic to provide a strongly-typed account of standard process calculus expressions of non-determinism. We show that our extension is expressive enough to capture many uses of non-determinism in untyped calculi, such as nondeterministic choice, while preserving HCP’s meta-theoretic properties, including deadlock freedom.

Original language	English
Title of host publication	Coordination Models and Languages
Subtitle of host publication	21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17–21, 2019, Proceedings
Editors	Hanne Riis Nielson, Emilio Tuosto
Publisher	Springer, Cham
Pages	37-53
Number of pages	18
Volume	11533
ISBN (Electronic)	978-3-030-22397-7
ISBN (Print)	978-3-030-22396-0
DOIs	https://doi.org/10.1007/978-3-030-22397-7_3
Publication status	Published - 8 Aug 2019
Event	21st IFIP WG 6.1 International Conference, COORDINATION 2019, International Conference on Coordination Models and Languages: Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17–21, 2019 - Technical University of Denmark, Copenhagen, Denmark Duration: 17 Jun 2019 → 21 Jun 2019 Conference number: 21 http://www.discotec.org/2019/coordination

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Cham
Volume	11533
ISSN (Print)	0302-9743

Conference

Conference	21st IFIP WG 6.1 International Conference, COORDINATION 2019, International Conference on Coordination Models and Languages
Abbreviated title	COORDINATION 2019
Country/Territory	Denmark
City	Copenhagen
Period	17/06/19 → 21/06/19
Internet address	http://www.discotec.org/2019/coordination

Keywords / Materials (for Non-textual outputs)

π -calculus
Linear logic
Session types
Non-determinism
Deadlock freedom

Access to Document

10.1007/978-3-030-22397-7_3Licence: All Rights Reserved

Towards Races in Linear_KOKKE_DoA180619_AFVAccepted author manuscript, 1.18 MBLicence: All Rights Reserved

https://rd.springer.com/chapter/10.1007/978-3-030-22397-7_3

From Data Types to Session Types - A Basis for Concurrency and Distribution
Wadler, P.
EPSRC
20/05/13 → 19/11/20
Project: Research

Cite this

Kokke, K., Morris, J. G., & Wadler, P. (2019). Towards Races in Linear Logic. In H. Riis Nielson, & E. Tuosto (Eds.), Coordination Models and Languages: 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17–21, 2019, Proceedings (Vol. 11533, pp. 37-53). (Lecture Notes in Computer Science; Vol. 11533). Springer, Cham. Advance online publication. https://doi.org/10.1007/978-3-030-22397-7_3

Kokke, Kerewin ; Morris, J. Garrett ; Wadler, Philip. / Towards Races in Linear Logic. Coordination Models and Languages: 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17–21, 2019, Proceedings. editor / Hanne Riis Nielson ; Emilio Tuosto. Vol. 11533 Springer, Cham, 2019. pp. 37-53 (Lecture Notes in Computer Science).

@inproceedings{d5df0286ee4e447ab2fb735fd5806cc2,

title = "Towards Races in Linear Logic",

abstract = "Process calculi based in logic, such as πDILL and CP, provide a foundation for deadlock-free concurrent programming, but exclude nondeterminism and races. HCP is a reformulation of CP which addresses a fundamental shortcoming: the fundamental operator for parallel composition from the π-calculus does not correspond to any rule of linear logic, and therefore not to any term construct in CP. We introduce HCP− ND, which extends HCP with a novel account of nondeterminism. Our approach draws on bounded linear logic to provide a strongly-typed account of standard process calculus expressions of non-determinism. We show that our extension is expressive enough to capture many uses of non-determinism in untyped calculi, such as nondeterministic choice, while preserving HCP{\textquoteright}s meta-theoretic properties, including deadlock freedom. ",

keywords = "π -calculus, Linear logic, Session types, Non-determinism, Deadlock freedom",

author = "Kerewin Kokke and Morris, {J. Garrett} and Philip Wadler",

year = "2019",

month = aug,

day = "8",

doi = "10.1007/978-3-030-22397-7_3",

language = "English",

isbn = "978-3-030-22396-0",

volume = "11533",

series = "Lecture Notes in Computer Science",

publisher = "Springer, Cham",

pages = "37--53",

editor = "{Riis Nielson}, Hanne and Emilio Tuosto",

booktitle = "Coordination Models and Languages",

note = "21st IFIP WG 6.1 International Conference, COORDINATION 2019, International Conference on Coordination Models and Languages : Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17–21, 2019, COORDINATION 2019 ; Conference date: 17-06-2019 Through 21-06-2019",

url = "http://www.discotec.org/2019/coordination",

}

Kokke, K, Morris, JG & Wadler, P 2019, Towards Races in Linear Logic. in H Riis Nielson & E Tuosto (eds), Coordination Models and Languages: 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17–21, 2019, Proceedings. vol. 11533, Lecture Notes in Computer Science, vol. 11533, Springer, Cham, pp. 37-53, 21st IFIP WG 6.1 International Conference, COORDINATION 2019, International Conference on Coordination Models and Languages, Copenhagen, Denmark, 17/06/19. https://doi.org/10.1007/978-3-030-22397-7_3

Towards Races in Linear Logic. / Kokke, Kerewin; Morris, J. Garrett ; Wadler, Philip.
Coordination Models and Languages: 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17–21, 2019, Proceedings. ed. / Hanne Riis Nielson; Emilio Tuosto. Vol. 11533 Springer, Cham, 2019. p. 37-53 (Lecture Notes in Computer Science; Vol. 11533).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Towards Races in Linear Logic

AU - Kokke, Kerewin

AU - Morris, J. Garrett

AU - Wadler, Philip

N1 - Conference code: 21

PY - 2019/8/8

Y1 - 2019/8/8

N2 - Process calculi based in logic, such as πDILL and CP, provide a foundation for deadlock-free concurrent programming, but exclude nondeterminism and races. HCP is a reformulation of CP which addresses a fundamental shortcoming: the fundamental operator for parallel composition from the π-calculus does not correspond to any rule of linear logic, and therefore not to any term construct in CP. We introduce HCP− ND, which extends HCP with a novel account of nondeterminism. Our approach draws on bounded linear logic to provide a strongly-typed account of standard process calculus expressions of non-determinism. We show that our extension is expressive enough to capture many uses of non-determinism in untyped calculi, such as nondeterministic choice, while preserving HCP’s meta-theoretic properties, including deadlock freedom.

AB - Process calculi based in logic, such as πDILL and CP, provide a foundation for deadlock-free concurrent programming, but exclude nondeterminism and races. HCP is a reformulation of CP which addresses a fundamental shortcoming: the fundamental operator for parallel composition from the π-calculus does not correspond to any rule of linear logic, and therefore not to any term construct in CP. We introduce HCP− ND, which extends HCP with a novel account of nondeterminism. Our approach draws on bounded linear logic to provide a strongly-typed account of standard process calculus expressions of non-determinism. We show that our extension is expressive enough to capture many uses of non-determinism in untyped calculi, such as nondeterministic choice, while preserving HCP’s meta-theoretic properties, including deadlock freedom.

KW - π -calculus

KW - Linear logic

KW - Session types

KW - Non-determinism

KW - Deadlock freedom

U2 - 10.1007/978-3-030-22397-7_3

DO - 10.1007/978-3-030-22397-7_3

M3 - Conference contribution

SN - 978-3-030-22396-0

VL - 11533

T3 - Lecture Notes in Computer Science

SP - 37

EP - 53

BT - Coordination Models and Languages

A2 - Riis Nielson, Hanne

A2 - Tuosto, Emilio

PB - Springer, Cham

T2 - 21st IFIP WG 6.1 International Conference, COORDINATION 2019, International Conference on Coordination Models and Languages

Y2 - 17 June 2019 through 21 June 2019

ER -

Kokke K, Morris JG, Wadler P. Towards Races in Linear Logic. In Riis Nielson H, Tuosto E, editors, Coordination Models and Languages: 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17–21, 2019, Proceedings. Vol. 11533. Springer, Cham. 2019. p. 37-53. (Lecture Notes in Computer Science). Epub 2019 Jun 5. doi: 10.1007/978-3-030-22397-7_3

Towards Races in Linear Logic

Abstract / Description of output

Publication series

Conference

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Projects

From Data Types to Session Types - A Basis for Concurrency and Distribution

Cite this