Kolmogorov's interpretation and a formal semantics of the meta-logic of intuitionistic logic

I would like to report on a formal semantics capturing Kolmogorov's informal interpretation of intuitionistic logic in terms of problem solving.
Kolmogorov's interpretation consists of two parts: one deals with the logical connectives and, implicitly, quantifiers, and is more or less the same as the so-called BHK interpretation; and the other deals with principles and rules and hence, implicitly, with the meta-logical connectives and quantifiers. The logical part has been extensively covered and discussed in the literature - albeit mostly in the terminology of Brouwer and Heyting, which forces a once-and-for-all choice between intuitionistic and classical logics despite their coexistence and interaction in Kolmogorov's approach. (Concerning this interaction see https://arxiv.org/abs/1312.2575 and https://arxiv.org/abs/1504.03379.)
By contrast, the meta-logical part has been neglected. This is not surprising, as it turns out to be incompatible with the usual model theory, based on Tarski's notion of semantic consequence; worse yet, it is an interpretation of something that does not exist in the usual formalism of first-order logic (but exists, for instance, in the meta-logical formalism of the Isabelle prover). However, ignoring the meta-logical part has the effect of throwing the baby out with the bathwater: as observed by Troelstra and van Dalen, "the BHK-interpretation in itself has no ‘explanatory power’ ", since "on a very ‘classical’ interpretation of [the informal notions of] construction and mapping," its six clauses "justify the principles of two-valued (classical) logic."
To address these issues, we develop a formal semantics of Isabelle's meta-logic, or rather of its simplified version which suffices for first-order logics without equality. In usual model theory, regarded as a particular semantics of the meta-logic, the meta-logical connectives and quantifiers are interpreted classically (and moreover in the two-valued way) — even though they are constructive. By interpreting them constructively, we get a generalized model theory, which covers, in particular, some realizability-type interpretations of intuitionistic logic.
On the other hand, Kolmogorov's interpretation of inference rules (which is a substantial part of his interpretation of intuitionistic logic, and seems to be uniquely possible in his approach) is based on a notion of semantic consequence that is alternative to Tarski's standard notion, and is incompatible even with the generalized model theory. Thus we develop an alternative model theory, which is nothing new for formulas and principles, but an entirely different interpretation of rules (and of more complex meta-logical constructs). By using an extension of the meta-logic, we further get a generalized alternative model theory, which suffices to formalize Kolmogorov's interpretation of rules. See https://arxiv.org/abs/1504.03380.
As a work in progress, we also develop a slightly different, "categorifed" semantics of the meta-logic, which in particular yields an interpretation of the meta-logic of (first-order) intuitionistic logic that has some intrinsic similarity with Voevodsky's interpretation of Martin-Löf's type theory with universes.