Gianluigi Ferrari, Eugenio Moggi and Rosario Pugliese

MetaKlaim - a Type Safe Multi-stage Language for Global Computing

This paper describes the design and the semantics of MetaKlaim, an 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 (like assembly and linking of code fragments), dynamic checking of security policies at administrative boundaries and “traditional” computational activities on a wide area network (like remote communication and code mobility). MetaKlaim exploits a powerful type system (including polymorphic types ´a la system F) to deal with highly parameterized mobile components and to dynamically enforce security policies: types are metadata which 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 are network applications are maintained whenever computations interoperate with potentially untrusted components.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

An Idealized MetaML

Very interesting! This reminds me that we never discussed An Idealized MetaML (AIM) from the same school.
In this paper, we present An Idealized MetaML (AIM) that is the result of our study of a categorical model for MetaML. An important outstanding problem is finding a type system that provides the user with a means for manipulating both open and closed code. This problem has eluded effrts by us and other researchers for over three years. AIM solves the issue by providing two type constructors, one classifies closed code and the other open code, and describing how they interact.
While being a big fan of concurrency, I think AIM paper is a good starting place fot those who think they are not ready to handle MetaKlaim wholesale.

Um, why am I thinking about Wittgenstein?... :-)