Meta-programming is a discipline of writing programs in a certain programming language that generate, manipulate or execute programs written in another language. In a typed setting, meta-programming languages usually contain a modal type constructor to distinguish the level of object programs (which are the manipulated data) from the meta programs (which perform the computations). In functional programming, modal types of object programs generally come in two flavors: open and closed, depending on whether the expressions they classify may contain any free variables or not. Closed object programs can be executed at run-time by the meta program, but the computations over them are more rigid, and typically produce less efficient residual code. Open object programs provide better inlining and partial evaluation, but once constructed, expressions of open modal type cannot be evaluated.

Recent work in this area has focused on combining the two notions into a sound type system. We present a novel calculus to achieve this, which we call nu-box. It is based on adding the notion of names inspired by the work on Nominal Logic and FreshML to the lambda-box 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, we extend our calculus with primitives for inspection and destruction of object programs at run-time in a type-safe manner.

40 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu