Types for resources in φ-calculi

Abstract

Several type systems have been proposed for characterizing resource usage in process calculi, starting with the work on linear and unbounded names in the -calculus by Kobayashi, Pierce and Turner. In this paper we use the general framework of -calculi proposed by Bengtson, Parrow et al. to provide a general theory of type systems of this kind. We present a general type system that allows for a subject reduction property generalizing that of Kobayashi et al. and show how existing, quite different type systems for resource control can be expressed within our general type system. These are the original type system for linear names in the -calculus, the graph types for strong normalization in the -calculus due to Honda, Yoshida and Berger, a type system for termination in a value-passing calculus due to Deng and Sangiorgi and a type system for allocation and deallocation of generated names due to de Vries, Francalanza and Hennessy. © Springer International Publishing Switzerland 2014.