Conference proceeding
Towards Races in Linear Logic
Lecture Notes in Computer Science, Vol.LNCS-11533, pp.37-53
Coordination Models and Languages
21th International Conference on Coordination Languages and Models (COORDINATION)
2019
DOI: 10.1007/978-3-030-22397-7_3
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.
Details
- Title: Subtitle
- Towards Races in Linear Logic
- Creators
- Wen Kokke - University of EdinburghJ Garrett Morris - Computer SciencePhilip Wadler - University of Edinburgh
- Resource Type
- Conference proceeding
- Publication Details
- Lecture Notes in Computer Science, Vol.LNCS-11533, pp.37-53
- Conference
- 21th International Conference on Coordination Languages and Models (COORDINATION)
- Series
- Coordination Models and Languages
- DOI
- 10.1007/978-3-030-22397-7_3
- ISSN
- 0302-9743
- eISSN
- 1611-3349
- Publisher
- Springer International Publishing
- Language
- English
- Date published
- 2019
- Academic Unit
- Computer Science
- Record Identifier
- 9984259467002771
Metrics
23 Record Views