Higher-Order Types and Meta-Programming for Global Computing

MetaKlaim 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-pro...

Full description

Saved in:
Bibliographic Details
Published in:Electronic notes in theoretical computer science 2002-06, Vol.62, p.52-68
Main Authors: Ferrari, G., Moggi, E., Pugliese, R.
Format: Article
Language:English
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:MetaKlaim 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.
ISSN:1571-0661
1571-0661
DOI:10.1016/S1571-0661(04)00319-6