Metaklaim: A type safe multi-stage language for global computing

This paper describes the design and semantics of MetaKlaim, which is a higher order distributed process calculus equipped with staging mechanisms. MetaKlaim integrates MetaML (an extension of SML for multi-stage programming) and Klaim (a Kernel Language for Agents Interaction and Mobility), to permit interleaving of meta-programming activities (such as assembly and linking of code fragments), dynamic checking of security policies at administrative boundaries and ‘traditional’ computational activities on a wide area network (such as remote communication and code mobility). MetaKlaim exploits a powerful type system (including polymorphic types a ́ la system F) to deal with highly parameterised mobile components and to enforce security policies dynamically: types are metadata that are extracted from code at run-time and are used to express trustiness guarantees. The dynamic type checking ensures that the trustiness guarantees of wide area network applications are maintained whenever computations interoperate with potentially untrusted components.