Ferrari, Gianluigi; Moggi, Eugenio; Pugliese, Rosario MetaKlaim: a type safe multi-stage language for global computing. (English) Zbl 1085.68013 Math. Struct. Comput. Sci. 14, No. 3, 367-395 (2004). Summary: 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 à 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. Cited in 1 Document MSC: 68N15 Theory of programming languages 68N18 Functional programming and lambda calculus 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) Software:Klava; MetaKlaim; KLAIM PDFBibTeX XMLCite \textit{G. Ferrari} et al., Math. Struct. Comput. Sci. 14, No. 3, 367--395 (2004; Zbl 1085.68013) Full Text: DOI