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 -> ('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.
As far as I know type correctness tends to be undecidable for interesting cases so clearly formal grammars cannot capture every type system you can think of.
I know that major compiler generators allow arbitrary predicates for rules that prevent a rule from being executed if the predicate does not evaluate to true, e.g.
{ type(e1) == type(e2) } (expression e1) '+' (expression e2). This concept can easily be formalized; appropriate restrictions on the allowed predicates then can yield decidability by LBAs.
Deciding such predicates is at least difficult with respect to runtime so I guess people tend to perform an iterative parsing, collecting information in phase $k$ in order to check feasibility in phase $k+1$. For instance, you can build up a name table in one pass and then check that all used variables are (visibly) declared in a second run.
