Pasalic. The role type equality in meta-programming. phd thesis pdf@Emir Pasalic's homepage

Introduction has background and taxonomy. Uses type equality (~GADTs) for scoping and typing discipline of object language programs.

Chen and Xi. Meta-Programming through Typeful Code Representation. ICFP 2003. pdf@citeseer

Their first-order typeful code representation allows manipulation of open terms but disallows the evaluation of free variables.

Davies and Pfenning. A modal analysis of staged computation. POPL 99 pdf@citeseer JACM 48(3):555–604, May 2001.

introduces “lambda box” calculus, uses a modal interpretation of object language types.