Higher-Order Types and Meta-Programming for Global Computing

AbstractMetaKlaim is a case study in modeling the spatial, temporal and security aspects necessary for global computing. MetaKlaim integrates MetaML (an extension of SML for multi-stage programming) and Klaim (à Kernel Language for Agents Interaction and Mobility), in order to allow interleaving of meta-programming activities (like assembly and linking of code fragments), security checks (like type-checking at administrative boundaries) and normal computational activities. The staging annotations of MetaML provide a fine-grain control of the temporal aspects, Klaim's primitives support location awareness, while the type system supports security through the use of global types (in combination with dynamic type-checking) and generic mobile code through the use of polymorphism (à la system F). The paper describes syntax, type system and operational semantics of MetaKlaim, states two type safety results, and exemplifies its use for describing mobile code applications