Usually in books such as Schaum's outline of theory and problems of tensor calculus by David Kay, the summation convention is introduced with notes and remarks, at best some warnings and identities are given.
I have the feeling that one can develop a formal system for this notation from which identities (simply) follow. If anything, the treatment of free and dummy variables reminds me very much of free and bound variables in untyped lambda calculus, while expanding a formula to 'full form' (where all dummy indices disappear) sounds very much like $\beta$-reduction.
If one recovers the range of the indices into a context like one does in natural deduction or typed lambda calculus, one could write something like:
$$ \{I=3,J=2\} \vdash a_{ij}b_i \to_{\beta} \Sigma_{j=1}^{2}\Sigma_{i=1}^{3} a_{ij}b_i \to_{\beta} \Sigma_{j=1}^{2} a_{1j}b_1+a_{2j}b_2+a_{3j}b_3 \to_{\beta} \cdots $$
So
$$ \{I=3,J=2\} \vdash a_{ij}b_i \twoheadrightarrow_{\beta} a_{11}b_1+a_{21}b_2+a_{31}b_3 + a_{12}b_1+a_{22}b_2+a_{32}b_3 $$
Similarly, the rules governing equivalence of formulas feel like $\alpha$-equivalence.
Has anyone treated the summation convention in this way, giving deduction-like formal manipulation/subsitution/reduction/equivalence rules?
First, looking at summation notation (not the summation convention), i.e. $\sum_{i=0}^N a_i$, this is just a binding form like many other binding forms that occur in mathematics besides the lambda calculus. For example, quantifiers in logic, and differentiation and integration in calculus as well as taking of limits, also indexed forms of union and intersection in set theory. In all of these cases, you could, if you wanted, instead view these constructs as higher-order functions. That is, instead of viewing summing as a binding form, you can view it as a function that takes a function, e.g. $\sum_{i=0}^N a_i$ becomes $\sum_{0,N}(\lambda i.a_i)$ (or even $\sum_{0,N}(a)$). Of course, you need to then define these higher-order functions, e.g. $$\sum_{i,N}(f) = \begin{cases}0,&\text{if }i > N \\f(i)+\sum_{i+1,N}(f),&\text{if }i\leq N\end{cases}$$
The summation convention, as the name suggests, is just a convention for implicitly binding variables. Once you insert the summation symbols, it reduces to just normal rules for binding forms. As you point out, it does require some contextual information to insert the bounds. One could imagine making some formal calculus that directly gave meaning to expression utilizing the summation convention without introducing summation symbols, but it would be somewhat tedious, a bit limiting, and mostly pointless.