We present an implementation of reflection for the Nuprl theorem prover, based on combining intuitions from programming languages and logical languages.
We reflect a logical language, adapting the common practice from Lisp dialects of avoiding redundant coding whenever it is possible to expose internal functionality. In particular, concepts of the logical language such as term syntax and substitution are directly reflected as primitives. The resulting notation has both the expressiveness and the simplicity needed for ordinary syntactic explanations and arguments.
The system is demonstrated by formalizing Tarski's result regarding the internal undefinability of a Truth predicate, closely following a standard "paper proof." We believe this shows to good effect our rather transparent quote-like notation, especially by exploiting colors.