Luca Cardelli
ABSTRACT
Java has demonstrated the utility of type systems for mobile code, and in particular their use and implications for security. Security properties rest on the fact that a well-typed Java program (or the corresponding verified bytecode) cannot cause certain kinds of damage.In this paper we provide a type system for mobile computation, that is, for computation that is continuously active before and after movement. We show that a well-typed mobile computation cannot cause certain kinds of run-time fault: it cannot cause the exchange of values of the wrong kind, anywhere in a mobile system.
- 1.Amadio, R. An asynchronous model of locality, failure, and process mobility. In COORDINATION'97, LNCS 1282, Springer. 1997. Google Scholar
Digital Library
- 2.Boudol, (3., Asynchrony and the 7z-calculus. Technical Report 1702, INRIA, Sophia-Antipolis, 1992.Google Scholar
- 3.Cardelli, L., Abstractions for Mobile Computation. 1998. To appear. (See www.luca.demon.co.uk.)Google Scholar
- 4.Cardelli, L. and A.D. Gordon, Mobile Ambients. In Foundations of Software Science and Computational Structures, Maurice Nivat (Ed.), LNCS 1378, 140-155, Springer. 1998. Google Scholar
- 5.De Nicola, R., G. Ferrari, M. Pugliese, Coordinating Mobile Agents via Blackboards and Access Rights. COORDINA- TION'97, LNCS 1282, 220-237, Springer. 1997. Google ScholarDigital Library
- 6.Honda., K. and M. Tokoro, An object calculus for asynchronous communication. Proc. ECOOP'91, LNCS 521, 133- 147, Springer Verlag, 1991. Google ScholarDigital Library
- 7.Kobayashi, N., B.C. Pierce, and D.N. Turner, Linearity and the Pi-Calculus. Proc ACM POPL'96, 358-371. 1996. Google ScholarDigital Library
- 8.Milner, R., J. Parrow and D. Walker, A calculus of mobile processes, Parts 1-2. Information and Computation, 100(1), 1-77. 1992. Google ScholarDigital Library
- 9.Odersky, M., Polarized Name Passing. Proc FST&TCS, Springer. 1995. Google ScholarDigital Library
- 10.Pierce, B., and D. Sangiorgi, Typing and Subtyping for Mobile Processes. Mathematical Structures in Computer Science, 6(5), 409-454. 1996.Google ScholarCross Ref
- 11.Riely, J. and M. Hennessy, A typed language for distributed mobile processes, in Proc A CM POPL'98, 378-390. 1998. Google ScholarDigital Library
- 12.Sewell, P., Global/Local Subtyping and Capability Inference for a Distributed n-calculus. In Proc ICALP'98, Springer. 1998. Google ScholarDigital Library
- 13.White, J.E., Mobile agents. In Software Agents, J. Bradshaw, ed. AAAI Press / The MIT Press. 1996.Google Scholar
Index Terms
- Types for mobile ambients
Recommendations
Qualified types for MLF
Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingMLF is a type system that extends a functional language with impredicative rank-n polymorphism. Type inference remains possible and only in some clearly defined situations, a local type annotation is required. Qualified types are a general concept that ...
Qualified types for MLF
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingMLF is a type system that extends a functional language with impredicative rank-n polymorphism. Type inference remains possible and only in some clearly defined situations, a local type annotation is required. Qualified types are a general concept that ...
Boxy types: inference for higher-rank types and impredicativity
ICFP '06: Proceedings of the eleventh ACM SIGPLAN international conference on Functional programmingLanguages with rich type systems are beginning to employ a blend of type inference and type checking, so that the type inference engine is guided by programmer-supplied type annotations. In this paper we show, for the first time, how to combine the ...
Comments