In A Self-Interpreter for F-omega, Brown and Palsberg construct for each term of each type $x:T$ a representation $\bar x : \Box T$ (a metatheoretical function which can't be represented in the language), and an interpretation function $u_T : \Box T \to T$. This is reminiscent of GL provability logic, which in particular abstracts how PA can represent its own proof theory. But while the representation looks like the axiom $\vdash T \implies \vdash \Box T$, the second $\vdash \Box T \to T$ is inconsistent with GL.
So what sort of gadget is this, in logical terms?
Can it be used at all to talk about the metatheory of F-omega?
What would a representation operation that satisfies the axioms of GL look like?