This rings a bell. And ah yes, on p. 48 of Sara Negri and Jan van Plato's admirable book Structural Proof Theory (CUP, 2001), they write
It is not the [general] feature of having a multiset as a succedent that leads
to classical logic, but the unrestricted $R\!\supset$ rule,
where by the unrestricted $R\!\supset$ they mean your classical $\to\! R$ rule, and the restricted rule would be your $\to\! R'$ rule.
Then on p. 108, they introduce an intuitionistic multisuccedent calculus they call G3im, which is exactly like a classical multisuccedent calculus except for the $\supset$ rules (though both left and right rules get tinkered with). I guess that the ensuing discussion, and the 1988 book by Dragalin Mathematical Intuitionism to which the calculus is due, would seem to be good starting points for further investigation (and I'd be interested to hear more about how things go!).
Gentzen [1] kick-started the field of structural proof theory: the 1934 paper introduces natural deduction. In the paper he already noted that introduction rules essentially represent definitions of the logical symbols. Later on, Gentzen took this perspective much further in his work on the sequent calculus, where he associates to each proof of a given sentence a corresponding canonical (cut-free) proof whose last rule has predictable form, depending only on the principal connective or quantifier of the formula.
Cut-elimination allows us to prove that intuitionistic logic satisfies structural properties (what you'd call metatheoretic properties, many of them tellingly named after the connectives) such as the disjunction property (if there is a proof of $A \vee B$, there ought to be a proof of $A$ or a proof of $B$), the conjunction property (if there is a proof of $A \wedge B$, there ought to be a proof of $A$ and a proof of $B$) and consistency (there ought to be no proof of $\bot$), and corresponding to the BHK interpretation of the connectives. In Gentzen's sequent calculus, we can prove all of them the same way: by considering the last rule of a canonical proof, which has to be a right rule for the connective. E.g. to prove the conjunction property, we can consider a proof of $\vdash A \wedge B$: by cut-elimination, we can turn this proof into a canonical proof, which must then have the last rule
$$\frac{\vdash A\ \ \ \ \vdash B}{\vdash A \wedge B} \wedge\!R$$
so we indeed have proofs of $\vdash A$ and $\vdash B$ as desired. Similarly, we have consistency: if $\vdash \bot$ had a proof, it would have a cut-free proof, but it obviously has no cut-free proof (what would be its last rule?!). The rules enunciate the BHK-style desiderata: cut-elimination ensures that we indeed get the desiderata. One can play a very similar game in natural deduction, using Prawitz's [2] proof normalization technique (indeed the right rules of the former correspond to introduction rules of the latter, and left rules similarly correspond to elimination rules).
This should give you some idea about the desiderata corresponding to the rules of natural deduction, and the proofs that establish that each of these are indeed met. For a more thorough appraisal and philosophical discussion, check out Francez's book on Proof-theoretic Semantics [3], especially his discussions of inferentialism, and of Prior's tonk connective. If you're more interested in the technical details of normalization, Parwitz [2] or Chapter 4 of Dummett [4] are good starting points as well.
[1] Gerhard Gentzen, "Untersuchungen über das logische Schließen. I". Mathematische Zeitschrift 39 (2), 1934.
[2] Dag Prawitz, "Natural Deduction: A Proof-Theoretical Study", Dover Publications 1965.
[3] Nissim Francez, "Proof-theoretic Semantics", Studies in Logic 57, College Publications UK, 2015.
[4] Michael Dummett, "Elements of intuitionism", Oxford Logic Guides 39, Oxford University Press, 1977.
Best Answer
For bi-conditional, I would suggest:
$\dfrac {\Gamma, A \vdash B \ \ \ \ \Gamma, B \vdash A}{\Gamma \vdash A \leftrightarrow B} \text { for }(\leftrightarrow \text I)$
and the pair:
$\dfrac {\Gamma \vdash A \leftrightarrow B}{\Gamma, A \vdash B} \ \ \ \dfrac {\Gamma \vdash A \leftrightarrow B}{\Gamma, B \vdash A} \text { for }(\leftrightarrow \text E)$
For exclusive or, the pair:
$\dfrac {\Gamma, A \vdash \ \ \ \ \Gamma \vdash B}{\Gamma \vdash A \oplus B} \ \ \ \dfrac {\Gamma, \vdash A \ \ \ \ \Gamma, B \vdash}{\Gamma \vdash A \oplus B} \text { for }(\oplus \text I)$
and the corresponding for $(\oplus \text E)$, based on the fact that an $\oplus$ True formula can produce cases: either $A$ False and $B$ True or the symmetric one:
$\dfrac {\Gamma, A \vdash \ \ \ \ \Gamma \vdash A \oplus B}{ \Gamma \vdash B} \ \ \ \dfrac {\Gamma, \vdash A \ \ \ \ \Gamma \vdash A \oplus B}{\Gamma, B \vdash}$