One can study the standard semantics of classical propositional logic within classical logic set theory, so we can say that the semantics of classical logic is meta-theoretically "self-hosting". This property is probably a big part of why classical logic is so easy to accept as the default/implicit background/foundational logic for mathematics.

In contrast, classical logic set theory is also used in the presentation of the mainstream semantic interpretations of propositional intuitionistic logic such as Kripke semantics and Heyting algebra. For example, in Kripke semantics our structures are triples $M = \langle W, \leq, v\rangle$ where $W \neq \varnothing$, $\leq$ is a preorder on $W$, and $v$ is a set function from the set of atomic propositions to the powerset of $W$, where $v$ must satisfy: for every $w_1,w_2 \in W$, for every atomic proposition $p$, if $w_1 \leq w_2$ and $w_1 \in v(p)$, then $w_2 \in v(p)$. So far, it seems that we could assume that we are working in some kind of intuitionistic set theory setting, however when we get to the definition of interpretation of formulas, it seems like there are some problems with using an intuitionistic meta-theory: \begin{array}{lll} M,w \vDash p &\text{ iff } &w \in v(p)\\ M,w \vDash \top\\ M,w \nvDash \bot\\ M,w \vDash \phi_1 \to \phi_2 &\text{ iff } &\text{for every } w'\in W.\text{ if } w \leq w' \text{ and } M,w' \vDash \phi_1 \text{ then } M,w' \vDash \phi_2\\ M,w \vDash \phi_1 \lor \phi_2 &\text{ iff } & M,w \vDash \phi_1 \text{ or } M,w \vDash \phi_2\\ M,w \vDash \phi_1 \land \phi_2 &\text{ iff } & M,w \vDash \phi_1 \text{ and } M,w \vDash \phi_2 \end{array} First off: now that we are interpreting this presentation in some kind of intuitionistic meta-theory, we will no longer necessarily have $w \vDash \phi$ or $w \nvDash \phi$, whereas before this would be true of every formula $\phi$, thanks to the law of excluded middle in classical logic. It seems like this may cause this semantics to determine a different logic than intuitionistic logic, when the meta-theory is taken to be intuitionistic.

Furthermore, in my experience with this semantic interpretation, there are many times where a formula is found to be semantically valid based on some use of the law of excluded middle. For example, you might observe that there must exist some future world $w$ such that $w \vDash \phi$, or else for every future world $w$ we must have $w \nvDash \phi$. This also indicates to me that using an intuitionistic meta-theory may cause the resulting logic to be different.

I haven't been able to find an example of a formula that would be intuitionistically valid, but not valid in the logic determined by Kripke semantics as interpreted within an intuitionistic meta-theory, but it seems like such a thing might exist.

Can anyone point me to any work that studies this issue in depth? Or point me to work that studies the more general issue of meta-theoretic "leakage" with respect to semantics?

Finally, if this is indeed a problem with Kripke/Heyting semantics, has anyone discovered a "self-hosting" intuitionistic semantics? Specifically: a semantic interpretation of intuitionistic propositional logic that assumes a meta-theory based on some kind of intuitionistic set theory, and is sound and complete with respect to a standard intuitionistic proof system.