Context Sensitive Grammars and Types 1) What, if any, is the relationship between static typing and formal grammars?

2) In particular, would it be possible for a linear bounded automaton to check whether, say, a C++ or SML program was well typed? A nested stack automaton?

3) Is there a natural way to express static typing rules in formal grammar terms?
It is not possible for linear bounded automata to check whether C++ programs, and unlikely to be possible for and LBA to check whether SML programs are well-typed. C++ has a Turing-complete type system, since you can code arbitrary programs as template metaprograms. 

SML is more interesting. It does have decidable type checking, but the problem is EXPTIME-complete. Hence it is unlikely an LBA can check it, unless there is a very surprising collapse in the complexity hierarchy. The reason for this is that SML requires type inference, and there are families of programs the size of whose type grows much faster than the size of the program. As an example, consider the following program:

fun delta x = (x, x)        (* this has type 'a -&gt; ('a * 'a), so its return value
                               has a type double the size of its argument *)

fun f1 x = delta (delta x)  (* Now we use functions to iterate this process *)
fun f2 x = f1 (f1 x)        
fun f3 x = f2 (f2 x)        (* This function has a HUGE type *)


For simpler type systems, such as C or Pascal's, I believe it is possible for an LBA to check it. 

In the early days of programming languages research, people sometimes used van Wingaarden grammars (aka two-level grammars) to specify type systems for programming languages. I believe Algol 68 was specified in this way. However, I am told this technique was abandoned for essentially pragmatic reasons: it turned out to be quite difficult for people to write grammars that specified what they thought they were specifying! (Typically, the grammars people wrote generated larger languages than they intended.) 

These days people use schematic inference rules to specify type systems, which is essentially a way of specifying predicates as the least fixed point of a collections of Horn clauses. Satisfiability for first-order Horn theories is undecidable in general, so if you want to capture everything type theorists do, then whatever grammatical formalism you choose will be stronger than is really convenient.

I know there has been some work on using attribute grammars to implement type systems. They claim there are some software engineering benefits for this choice: namely, attribute grammars control information flow very strictly, and I am told this makes program understanding  easier.