Towards Races in Linear Logic - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

Towards Races in Linear Logic

Wen Kokke
  • Fonction : Auteur
  • PersonId : 1058372
J. Garrett Morris
  • Fonction : Auteur
  • PersonId : 1058373
Philip Wadler
  • Fonction : Auteur
  • PersonId : 1058374

Résumé

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
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

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

Licence

Paternité

Identifiants

Citer

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⟩
31 Consultations
13 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More