What is the proof-theoretic significance of the existence of a Brown-Palsberg self-interpreter for system $F_\omega$? 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?
There is no proof significance, since already Gödel's $T$ has a Brown-Palsberg self-interpreter for free. We need a better definition of a typed self-interpreter.