Reference request: Proof theory in $W_1^1$

Question

Buss defined $V_2^1$​ as a second-order bounded arithmetic corresponding to $\mathsf{PSPACE}$. Later, Skelley introduced $W_1^1$​, a third-order bounded arithmetic of $\mathsf{PSPACE}$. Since the question $\mathsf{P =^? PSPACE}$ is still open, I think proof theory, especially incompleteness theorem related results in $V_2^1$ and $W_1^1$​, deserves more attention. Similar ideas have already been studied a lot in the context of $S_2^i$ and $T_2^i$.