Static analysis of multi-staged programs via unstaging translation

Static analysis of multi-staged programs via unstaging translation
W. Choi, B. Aktemur, K. Yi, and M. Tatsuta
POPL 2011

Staged programs are programs that construct and run other programs (written using the same syntax).  For example, Lisp's quote, antiquote and eval operations are well-known examples of .  In the typed programming world, MetaML and MetaOCaml may be the best-known language designs for staged computation.  Work on modal type systems (dating to Davies and Pfenning) established that one can view the modal $\Box$ type as a "code" type, with $run : \Box A \to A$.  Subsequent work has looked at modal types indexed by contexts (e.g. Contextual Modal Type Theory or Taha and Nielsen's environment classifiers).

This paper looks at the problem of static analysis for staged computation.  This is challenging because the values of code types are program fragments that may not be known until runtime, hence, it is difficult (or at least requires significant effort) to adapt classic static analysis techniques.  The authors argue that there has been no significant work on static analyses that are more detailed than type systems (and I don't know of any either).

The authors propose a solution based on translation.  A staged program (in a monomorphic $\lambda$-calculus with $box$, $unbox$ and $run$ operations) is translated to a conventional program in a $\lambda$-calculus with records.  A box type $\Box(\Gamma \vdash \tau)$ is translated to a function type $\tau_\Gamma \to \tau'$, where $\tau_\Gamma$ is a record with one field corresponding to each variable in $\Gamma$.  Boxing and unboxing are translated to function abstraction and application respectively.  Importantly, to preserve evaluation order, unboxing operations are "hoisted" outside of the $\lambda$-abstractions introduced by boxing.
Read more »