A Modality for Safe Resource Sharing and Code Reentrancy
The potential of linear logic in facilitating reasoning on resource usage has long been recognized. However, convincing uses of linear types in practical programming are still rather rare. In this paper, the authors present a general design to effectively support practical programming with linear types. In particular, they introduce and then formalize a modality, which they refer to as the sharing modality, in support of sharing of linear resources (with no use of locks). They develop the underlying type theory for the sharing modality and establish its soundness based on a notion of types with effects.