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.
| Original language | English |
|---|---|
| Title of host publication | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Number of pages | 20 |
| Volume | 8358 LNCS |
| Publisher | Springer |
| Publication date | 1 Jan 2014 |
| Pages | 83-102 |
| ISBN (Print) | 9783319051185 |
| DOIs | |
| Publication status | Published - 1 Jan 2014 |
| Event | 8th International Symposium on Trustworthy Global Computing - Buenos Aires, Argentina Duration: 30 Aug 2013 → 31 Aug 2013 Conference number: 8th |
Conference
| Conference | 8th International Symposium on Trustworthy Global Computing |
|---|---|
| Number | 8th |
| Country/Territory | Argentina |
| City | Buenos Aires |
| Period | 30/08/2013 → 31/08/2013 |
| Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 8358 LNCS |
| ISSN | 0302-9743 |