Computer Science Department
School of Computer Science, Carnegie Mellon University
Meta-Programming with Names and Necessity
This report was significantly revised in November 2002
Recent work in this area has focused on combining the two notions into a sound system. We present a novel way to achieve this. It is based on adding the notion of names from the work on Nominal Logic and FreshML to the LambdaBox-calculus of proof terms for the necessity fragment of modal logic S4. The resulting language provides a more fine-grained control over free variables of object programs when compared to the existing languages for meta-programming.
In addition, this approach lends itself well to addition of intensional code analysis, i.e., capability of meta programs to inspect and destruct object programs at run-time in a type-safe manner, which we also undertake.