Towards Races in Linear Logic

Kerewin Kokke, J. Garrett Morris, Philip Wadler

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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’s meta-theoretic properties, including deadlock freedom.
Original languageEnglish
Title of host publicationCoordination Models and Languages
Subtitle of host publication21st 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
EditorsHanne Riis Nielson, Emilio Tuosto
PublisherSpringer, Cham
Pages37-53
Number of pages18
Volume11533
ISBN (Electronic)978-3-030-22397-7
ISBN (Print)978-3-030-22396-0
DOIs
Publication statusPublished - 8 Aug 2019
Event21st 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 201921 Jun 2019
Conference number: 21
http://www.discotec.org/2019/coordination

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Cham
Volume11533
ISSN (Print)0302-9743

Conference

Conference21st IFIP WG 6.1 International Conference, COORDINATION 2019, International Conference on Coordination Models and Languages
Abbreviated titleCOORDINATION 2019
Country/TerritoryDenmark
CityCopenhagen
Period17/06/1921/06/19
Internet address

Keywords

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

Fingerprint

Dive into the research topics of 'Towards Races in Linear Logic'. Together they form a unique fingerprint.

Cite this