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 non-determinism 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 non-deterministic HCP, 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.
Cite
@article{arxiv.1909.13376,
title = {Towards Races in Linear Logic},
author = {Wen Kokke and J. Garrett Morris and Philip Wadler},
journal= {arXiv preprint arXiv:1909.13376},
year = {2023}
}