Abstract
This paper presents the Kell calculus, a family of distributed process calculi, parameterized by languages for input patterns, that is intended as a basis for studying component-based distributed programming. The Kell calculus is built around a π-calculus core, and follows five design principles which are essential for a foundational model of distributed and mobile programming: hierarchical localities, local actions, higher-order communication, programmable membranes, and dynamic binding. The paper discusses these principles, and defines the syntax and operational semantics common to all calculi in the Kell calculus family. The paper provides a co-inductive characterization of contextual equivalence for Kell calculi, under sufficient conditions on pattern languages, by means of a form of higher-order bisimulation called strong context bisimulation. The paper also contains several examples that illustrate the expressive power of Kell calculi.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aldrich, J., Chambers, C., Notkin, D.: Architectural Reasoning in ArchJava. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, p. 334. Springer, Heidelberg (2002)
Amadio, R.: An asynchronous model of locality, failure, and process mobility. Technical report, INRIA RR-3109, INRIA Sophia-Antipolis, France (1997)
Barbanera, F., Bugliesi, M., Dezani-Ciancaglini, M., Sassone, V.: A calculus of bounded capacities. In: Saraswat, V.A. (ed.) ASIAN 2003. LNCS, vol. 2896, pp. 205–223. Springer, Heidelberg (2003)
Boudol, G.: A Generic Membrane Model. In: Priami, C., Quaglia, P. (eds.) GC 2004. LNCS, vol. 3267, pp. 208–222. Springer, Heidelberg (2005)
Bruneton, E., Quéma, V., Coupaye, T., Leclercq, M., Stefani, J.B.: An Open Component Model and its Support in Java. In: Crnković, I., Stafford, J.A., Schmidt, H.W., Wallnau, K. (eds.) CBSE 2004. LNCS, vol. 3054, pp. 7–22. Springer, Heidelberg (2004)
Bugliesi, M., Castagna, G., Crafa, S.: Boxed ambients. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, p. 38. Springer, Heidelberg (2001)
Bugliesi, M., Crafa, S., Merro, M., Sassone, V.: Communication Interference in Mobile Boxed Ambients. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 71–84. Springer, Heidelberg (2002)
Carbone, M., Maffeis, S.: On the Expressive Power of Polyadic Synchronization in π-calculus. Electronic Notes in Theorectical Computer Science 68(2) (2002)
Cardelli, L., Gordon, A.: Mobile Ambients. Theoretical Computer Science 240(1) (2000)
Castagna, G., Zappa, F.: The Seal Calculus Revisited. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 85–96. Springer, Heidelberg (2002)
Castellani, I.: Process algebras with localities. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra. Elsevier, Amsterdam (2001)
Clarke, D., Wrigstad, T.: External Uniqueness is Unique Enough. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743. Springer, Heidelberg (2003)
Coppo, M., Dezani-Ciancaglini, M., Giovannetti, E., Salvo, I.: M 3: Mobility types for mobile processes in mobile ambients. In: CATS 2003. ENTCS, vol. 78 (2003)
Dal-Zilio, S.: Mobile Processes: A Commented Bibliography. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol. 2067, p. 206. Springer, Heidelberg (2001)
Fournet, C.: The Join-Calculus. PhD thesis, Ecole Polytechnique, Palaiseau, France (1998)
Fournet, C., Gonthier, G., Levy, J.J., Maranget, L., Remy, D.: A calculus of mobile agents. In: CONCUR 1996. LNCS, vol. 1119. Springer, Heidelberg (1996)
Godskesen, J.C., Hildebrandt, T., Sassone, V.: A calculus of mobile resources. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, p. 272. Springer, Heidelberg (2002)
Hennessy, M., Rathke, J., Yoshida, N.: Safedpi: a language for controlling mobile code. Technical Report 2003:02, University of Sussex (2003); Extended abstract presented at Foundations of Software Science and Computation Structures - 7th International Conference, FOSSACS 2004 (2004)
Hennessy, M., Riely, J.: Resource access control in systems of mobile agents. Technical report, Technical Report 2/98 – School of Cognitive and Computer Sciences, University of Sussex, UK (1998)
Jeffrey, A., Rathke, J.: Contextual equivalence for higher-order π-calculus revisited. In: Proceedings, 19th Conference on the Mathematical Foundations of Programming Semantics (2003)
Leavens, G., Sitaraman, M. (eds.): Foundations of Component-Based Systems. Cambridge University Press, Cambridge (2000)
Leth, L., Thomsen, B.: Some facile chemistry. Formal Aspects of Computing 7(3) (1995)
Levi, F., Sangiorgi, D.: Controlling interference in ambients. In: Proceedings 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2000) (2000)
Lynch, N.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)
Medvidovic, N., Taylor, R.N.: A Classification and Comparison Framework for Software Architecture Description Languages. Transactions on Software Engineering 26(1) (2000)
Merro, M., Hennessy, M.: Bisimulation congruences in safe ambients. In: 29th ACM Symposium on Principles of Programming Languages (POPL), Portland, Oregon, January 16-18 (2002)
Milner, R.: Communicating and mobile systems: The π-calculus. Cambridge University Press, Cambridge (1999)
De Nicola, R., Ferrari, G.L., Pugliese, R.: Klaim: a Kernel Language for Agents Interaction and Mobility. IEEE Trans. on Software Engineering 24(5) (1998)
De Nicola, R., Ferrari, G.L., Pugliese, R., Venneri, B.: Types for Access Control. Theoretical Computer Science 240(1) (2000)
Ravara, A., Matos, A., Vasconcelos, V., Lopes, L.: Lexically scoping distribution: what you see is what you get. In: FGC: Foundations of Global Computing. ENTCS, vol. 85(1). Elsevier, Amsterdam (2003)
Sangiorgi, D.: Bisimulation for higher-order process calculi. Information and Computation 131(2) (1996)
Sangiorgi, D., Walker, D.: The π-calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)
Schmitt, A., Stefani, J.B.: The M-calculus: A Higher-Order Distributed Process Calculus. In: Proceedings 30th Annual ACM Symposium on Principles of Programming Languages (POPL) (2003)
Sewell, P., Vitek, J.: Secure Composition of Insecure Components. Journal of Computer Security (2000); invited submission for a CSFW00 special issue
Stefani, J.B.: A calculus of kells. In: Sassone, V. (ed.) Proceedings International Workshop on Foundations of Global Computing. Electronic Notes in Theoretical Computer Science, vol. 85(1). Elsevier, Amsterdam (2003)
Thomsen, B.: A Theory of Higher Order Communicating Systems. Information and Computation 116(1) (1995)
Vasconcelos, V.T.: A note on a typing system for the higher-order π-calculus (September 1993)
Wojciechowski, P., Sewell, P.: Nomadic Pict: Language and Infrastructure. IEEE Concurrency 8(2) (2000)
Yoshida, N., Hennessy, M.: Assigning types to processes. In: 15th Annual IEEE Symposium on Logic in Computer Science (LICS) (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schmitt, A., Stefani, JB. (2005). The Kell Calculus: A Family of Higher-Order Distributed Process Calculi. In: Priami, C., Quaglia, P. (eds) Global Computing. GC 2004. Lecture Notes in Computer Science, vol 3267. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31794-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-31794-4_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24101-0
Online ISBN: 978-3-540-31794-4
eBook Packages: Computer ScienceComputer Science (R0)