Towards Races in Linear Logic - Coordination Models and Languages
Conference Papers Year : 2019

Towards Races in Linear Logic

Wen Kokke
  • Function : Author
  • PersonId : 1058372
J. Garrett Morris
  • Function : Author
  • PersonId : 1058373
Philip Wadler
  • Function : Author
  • PersonId : 1058374

Abstract

Process calculi based in logic, such as $\pi $DILL and CP, provide a foundation for deadlock-free concurrent programming, but exclude non-determinism and races. HCP is a reformulation of CP which addresses a fundamental shortcoming: the fundamental operator for parallel composition from the $\pi $-calculus does not correspond to any rule of linear logic, and therefore not to any term construct in CP. We introduce HCP${-} _{\text {ND}}$, which extends HCP with a novel account of non-determinism. 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 non-deterministic choice, while preserving HCP ’s meta-theoretic properties, including deadlock freedom.
Fichier principal
Vignette du fichier
478673_1_En_3_Chapter.pdf (1.18 Mo) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

hal-02365505 , version 1 (15-11-2019)

Licence

Identifiers

Cite

Wen Kokke, J. Garrett Morris, Philip Wadler. Towards Races in Linear Logic. 21th International Conference on Coordination Languages and Models (COORDINATION), Jun 2019, Kongens Lyngby, Denmark. pp.37-53, ⟨10.1007/978-3-030-22397-7_3⟩. ⟨hal-02365505⟩
57 View
40 Download

Altmetric

Share

More