×

Spatial-behavioral types, distributed services, and resources. (English) Zbl 1211.68026

Montanari, Ugo (ed.) et al., Trustworthy global computing. Second symposium, TGC 2006, Lucca, Italy, November 7-9, 2006. Revised selected papers. Berlin: Springer (ISBN 978-3-540-75333-9/pbk). Lecture Notes in Computer Science 4661, 98-115 (2007).
Summary: We develop a notion of spatial-behavioral typing suitable to discipline interactions in service-based systems modeled in a distributed object calculus. Our type structure reflects a resource aware model of behavior, where a parallel composition type operator expresses resource independence, a sequential composition type operator expresses implicit synchronization, and a modal operator expresses resource ownership. Soundness of our type system is established using a logical relations technique, building on a interpretation of types as properties expressible in a spatial logic.
For the entire collection see [Zbl 1129.68006].

MSC:

68M14 Distributed systems
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

SLMC; PIPER
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M., Cardelli, L.: A theory of primitive objects: Untyped and first-order systems. Inf. Comput. 125(2) (1996) · Zbl 0853.68115
[2] Bartoletti, M.; Degano, P.; Ferrari, G., Enforcing secure service composition, 18th IEEE Computer Security Foundations Workshop (CSFW-18 2005), 211-223 (2005), Los Alamitos: IEEE Computer Society, Los Alamitos · doi:10.1109/CSFW.2005.17
[3] Di Blasio, P.; Fisher, K.; Sassone, V.; Montanari, U., A calculus for concurrent objects, CONCUR ’96: Concurrency Theory, 655-670 (1996), Heidelberg: Springer, Heidelberg · Zbl 1514.68163
[4] Boyapati, C., Liskov, B., Shrira, L.: Ownership types for object encapsulation. In: Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2003) · Zbl 1321.68166
[5] Caires, L.; Walukiewicz, I., Behavioral and Spatial Properties in a Logic for the Pi-Calculus, Foundations of Software Science and Computation Structures (2004), Heidelberg: Springer, Heidelberg
[6] Caires, L.; Cardelli, L., A Spatial Logic for Concurrency (Part I), Information and Computation, 186, 2, 194-235 (2003) · Zbl 1068.03022 · doi:10.1016/S0890-5401(03)00137-8
[7] Caires, L.; Cardelli, L., A Spatial Logic for Concurrency (Part II), Theoretical Computer Science, 3, 322, 517-565 (2004) · Zbl 1050.68104 · doi:10.1016/j.tcs.2003.10.041
[8] Cardelli, L.; Gordon, A. D., Anytime, Anywhere. Modal Logics for Mobile Ambients, 27th ACM Symp. on Principles of Programming Languages, 365-377 (2000), New York: ACM, New York · Zbl 1323.68405 · doi:10.1145/325694.325742
[9] Castagna, G.; De Nicola, R.; Varacca, D., Semantic subtyping for the π-calculus, 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 92-101 (2005), Los Alamitos: IEEE Computer Society, Los Alamitos · doi:10.1109/LICS.2005.46
[10] Chaki, S., Rajamani, S.K., Rehof, J.: Types as models: model checking message-passing programs. In: Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 45-57 (2002) · Zbl 1323.68365
[11] Clarke, D.G., Drossopoulou, S.: Ownership, encapsulation and the disjointness of type and effect. In: Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2002, pp. 292-310 (2002)
[12] Boreale, M., SCC: a Service Centered Calculus, Proceedings of WS-FM 2006, 3rd International Workshop on Web Services and Formal Methods (2006), Heidelberg: Springer, Heidelberg
[13] Gordon, A.D., Hankin, P.D.: A concurrent object calculus: Reduction and typing. Electr. Notes Theor. Comput. Sci. 16(3) (1998) · Zbl 0917.68064
[14] Hennessy, M.; Riely, J., Resource access control in systems of mobile agents, Inf. Comput., 173, 1, 82-120 (2002) · Zbl 1009.68081 · doi:10.1006/inco.2001.3089
[15] Honda, K.; Vasconcelos, V. T.; Kubo, M.; Hankin, C., Language primitives and type discipline for structured communication-based programming, Programming Languages and Systems - ESOP’98, 122-138 (1998), Heidelberg: Springer, Heidelberg · doi:10.1007/BFb0053567
[16] Igarashi, A., Kobayashi, N.: A generic type system for the pi-calculus. In: POPL 2001: 28th Annual Symposium on Principles of Programming Languages (2001) · Zbl 1323.68410
[17] Igarashi, A., Kobayashi, N.: Resource usage analysis. In: POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 331-342 (2002) · Zbl 1323.68377
[18] Misra, J., Cook, W.R.: Computation orchestration: A basis for wide-area computing. Journal of Software and Systems Modeling (2006)
[19] O’Hearn, P. W.; Gardner, P.; Yoshida, N., Resources, concurrency and local reasoning, CONCUR 2004 - Concurrency Theory, 49-67 (2004), Heidelberg: Springer, Heidelberg · Zbl 1099.68588
[20] Reynolds, J. C., Separation Logic: A Logic for Shared Mutable Data Structures, Third Annual Symposium on Logic in Computer Science (2002), Los Alamitos: IEEE Computer Society, Los Alamitos
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.