This document describes part of an effort to achieve in Nuprl a practical reflection of its expression syntax. This reflection is done at the granularity of the operators; in particular, each operator of the syntax is denoted by another operator of the same syntax. Further, the syntax has binding operators, and we organize reflection not around the concrete binding syntax, but instead, around the abstract higher-order syntax. We formulate and prove the correctness of a core rule for inferring well-formedness of instances of operator-denoting operators.

There is also a list of HOAS Articles and a Citation Graph for them; most are not cited in the above paper.