Downloads provided by UsageCounts
Binary session types guarantee communication safety and session fidelity, but alone they cannot rule out deadlocks arising from the interleaving of different sessions. In Classical Processes (CP)$-$a process calculus based on classical linear logic$-$deadlock freedom is guaranteed by combining channel creation and parallel composition under the same logical cut rule. Similarly, in Good Variation (GV)$-$a linear concurrent $\lambda$-calculus$-$deadlock freedom is guaranteed by combining channel creation and thread spawning under the same operation, called fork. In both CP and GV, deadlock freedom is achieved at the expense of expressivity, as the only processes allowed are tree-structured. Dardha and Gay define Priority CP (PCP), which allows cyclic-structured processes and restores deadlock freedom by using priorities, in line with Kobayashi and Padovani. Following PCP, we present Priority GV (PGV), a variant of GV which decouples channel creation from thread spawning. Consequently, we type cyclic-structured processes and restore deadlock freedom by using priorities. We show that our type system is sound by proving subject reduction and progress. We define an encoding from PCP to PGV and prove that the encoding preserves typing and is sound and complete with respect to the operational semantics.
QA75, FOS: Computer and information sciences, BC1-199, Computer Science - Programming Languages, Logic, Electronic computers. Computer science, computer science - programming languages, QA75.5-76.95, Programming Languages (cs.PL)
QA75, FOS: Computer and information sciences, BC1-199, Computer Science - Programming Languages, Logic, Electronic computers. Computer science, computer science - programming languages, QA75.5-76.95, Programming Languages (cs.PL)
| citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 5 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
| downloads | 2 |

Downloads provided by UsageCounts