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.
Originalsprog | Engelsk |
---|---|
Titel | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
Antal sider | 20 |
Vol/bind | 8358 LNCS |
Forlag | Springer |
Publikationsdato | 1 jan. 2014 |
Sider | 83-102 |
ISBN (Trykt) | 9783319051185 |
DOI | |
Status | Udgivet - 1 jan. 2014 |
Begivenhed | 8th International Symposium on Trustworthy Global Computing - Buenos Aires, Argentina Varighed: 30 aug. 2013 → 31 aug. 2013 Konferencens nummer: 8th |
Konference
Konference | 8th International Symposium on Trustworthy Global Computing |
---|---|
Nummer | 8th |
Land/Område | Argentina |
By | Buenos Aires |
Periode | 30/08/2013 → 31/08/2013 |
Navn | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Vol/bind | 8358 LNCS |
ISSN | 0302-9743 |