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 - 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.
CITATION STYLE
Kokke, W., Morris, J. G., & Wadler, P. (2019). Towards races in linear logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11533 LNCS, pp. 37–53). Springer Verlag. https://doi.org/10.1007/978-3-030-22397-7_3
Mendeley helps you to discover research relevant for your work.