The proof-theoretic strength of Constructive Second-order set theories

In this paper, we define constructive analogues of second-order set theories, which we will call $\mathsf{I}\mathsf{G}\mathsf{B}$, $\mathsf{C}\mathsf{G}\mathsf{B}$, $\mathsf{I}\mathsf{K}\mathsf{M}$, and $\mathsf{C}\mathsf{K}\mathsf{M}$. Each of them can be viewed as $\mathsf{I}\mathsf{Z}\mathsf{F}$- and $\mathsf{C}\mathsf{Z}\mathsf{F}$-analogues of Gödel-Bernays set theory $\mathsf{G}\mathsf{B}$ and Kelley-Morse set theory $\mathsf{K}\mathsf{M}$. We also provide their proof-theoretic strengths in terms of classical theories, and we especially prove that $\mathsf{C}\mathsf{K}\mathsf{M}$ and full Second-Order Arithmetic have the same proof-theoretic strength.