Abstract
Many different mobile process calculi have been invented, and for each some number of type systems has been developed. Soundness and other properties must be proved separately for each calculus and type system. We present the generic polymorphic type system Poly* which works for a wide range of mobile process calculi, including the π-calculus and Mobile Ambients. For any calculus satisfying some general syntactic conditions, well-formedness rules for types are derived automatically from the reduction rules and Poly* works otherwise unchanged. The derived type system is automatically sound (i.e., has subject reduction) and often more precise than previous type systems for the calculus, due to Poly*’s spatial polymorphism. We present an implemented type inference algorithm for Poly* which automatically constructs a typing given a set of reduction rules and a term to be typed. The generated typings are principal with respect to certain natural type shape constraints.
Supported by EC FP5/IST/FET grant IST-2001-33477 “DART”, and Sun Microsystems equipment grant EDUD-7826-990410-US.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Inform. & Comput. 148(1) (1999)
Amtoft, T., Makholm, H., Wells, J.B.: PolyA: True type polymorphism for Mobile Ambients. In: IFIP TC1 3rd Int’l Conf. Theoret. Comput. Sci. (TCS 2004). Kluwer Academic Publishers, Dordrecht (2004)
Amtoft, T., Turbak, F.: Faithful translations between polyvariant flows and polymorphic types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, p. 26. Springer, Heidelberg (2000)
Boudol, G.: The π-calculus in direct style. In: Conf. Rec. POPL 1997: 24th ACM Symp. Princ. of Prog. Langs. (1997)
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: FST & TCS 2002 (2002)
Cardelli, L., Ghelli, G., Gordon, A.D.: Mobility types for mobile ambients. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, Springer, Heidelberg (1999); Extended version appears as Microsoft Research Technical Report MSR-TR-99-32 (1999)
Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, p. 140. Springer, Heidelberg (1998)
Cardelli, L., Wegner, P.: On understanding types, data abstraction, and polymorphism. Computing Surveys 17(4) (1985)
Castagna, G., Ghelli, G., Nardelli, F.Z.: Typing mobility in the Seal calculus. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, p. 82. Springer, Heidelberg (2001)
Chaki, S., Rajamani, S.K., Rehof, J.: Types as models: Model checking message-passing programs. In: Conf. Rec. POPL 2002: 29th ACM Symp. Princ. of Prog. Langs. (2002)
Coppo, M., Dezani-Ciancaglini, M., Giovannetti, E., Salvo, I.: M3: Mobility types for mobile processes in mobile ambients. In: CATS 2003. ENTCS, vol. 78 (2003)
Gordon, A.D., Jeffrey, A.S.A.: Typing correspondence assertions for communication protocols. Theoret. Comput. Sci. 300(1–3) (2003)
Igarashi, A., Kobayashi, N.: A generic type system for the pi-calculus. In: Conf. Rec. POPL 2001: 28th ACM Symp. Princ. of Prog. Langs. (2001)
Levi, F., Bodei, C.: A control flow analysis for safe and boxed ambients. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 188–203. Springer, Heidelberg (2004)
Levi, F., Sangiorgi, D.: Controlling interference in ambients. In: POPL 2000, Boston, Massachusetts. ACM Press, New York (2000)
Makholm, H., Wells, J.B.: Instant polymorphic type systems for mobile process calculi: Just add reduction rules and close. Technical Report HW-MACS-TR-0022, Heriot-Watt Univ., School of Math. & Comput. Sci. (2004)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. Inform. & Comput. 100(1) (1992)
Nielson, H.R., Nielson, F., Pilegaard, H.: Spatial analysis of BioAmbients. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 69–83. Springer, Heidelberg (2004)
Palsberg, J., Pavlopoulou, C.: From polyvariant flow information to intersection and union types. J. Funct. Programming 11(3) (2001)
Pericas-Geertsen, S.M.: XML-Fluent Mobile Ambients. PhD thesis, Boston University (2001)
Phillips, I., Vigliotti, M.G.: On reduction semantics for the push and pull ambient calculus. In: Theoretical Computer Science: 2nd IFIP Int’l Conf. IFIP Conference Proceedings, vol. 223. Kluwer Academic Publishers, Dordrecht (2002)
Sander, G.: Graph layout through the VCG tool. In: Tamassia, R., Tollis, I.G. (eds.) GD 1994. LNCS, vol. 894. Springer, Heidelberg (1995)
Turner, D.N.: The Polymorphic Pi-Calculus: Theory and Implementation. PhD thesis, University of Edinburgh, Report no ECS-LFCS-96-345 (1995)
Vitek, J., Castagna, G.: Seal: A framework for secure mobile computations. In: Bal, H.E., Cardelli, L., Belkhouche, B. (eds.) ICCL-WS 1998. LNCS, vol. 1686, p. 47. Springer, Heidelberg (1999)
Wells, J.B.: The essence of principal typings. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, p. 913. Springer, Heidelberg (2002)
Yoshida, N.: Graph types for monadic mobile processes. In: Chandru, V., Vinay, V. (eds.) FSTTCS 1996. LNCS, vol. 1180. Springer, Heidelberg (1996)
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
Makholm, H., Wells, J.B. (2005). Instant Polymorphic Type Systems for Mobile Process Calculi: Just Add Reduction Rules and Close. In: Sagiv, M. (eds) Programming Languages and Systems. ESOP 2005. Lecture Notes in Computer Science, vol 3444. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31987-0_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-31987-0_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25435-5
Online ISBN: 978-3-540-31987-0
eBook Packages: Computer ScienceComputer Science (R0)