CMU-CS-02-123RComputer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-02-123R
Aleksandar Nanevski November 2002
CMU-CS-02-123R.ps
Keywords: Meta-programming, modal logic, nominal logic, higher-order
abstract syntax, staged computation, run-time code generation, symbolic
computation
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 This page maintained by reports@cs.cmu.edu |