What is the theoretical basis of imperative programming? Functional programming has a theoretical basis in lambda calculus and combinatory logic.  As someone involved with statistical computing, I find these concepts to be very useful for modeling.

Is there an equivalent mathematical basis of imperative programming, or did it simply grow out of practical hardware application in machine language and the subsequent development of FORTRAN?
In general, when mathematics is used to study some X, one first needs a model of X, and then develops a theory, a set of results about that model. I guess that theory may be said to be a "theoretical basis" for X. Now set X=computation. There are many models of computation, many involving "state". Each model has its own "theory" and it is sometimes possible to "translate" between models. I believe it's hard to say which model is more "basic"---they are simply designed with different goals in mind.

Turing machines were designed to define what is computable. So they make a good model if you care about whether there exists an algorithm for a certain problem. This model is sometimes abused to study the efficiency of algorithms or the hardness of problems, under the pretext that it's good enough, at least if you only care about polynomial/non-polynomial. The RAM model is closer to a real computer and therefore better if you want a precise analysis of an algorithm. To put lower bounds on the hardness of problems it is better to not use a model that resembles too much today's computers because you want to cover a wide range of possible computers, while still being more precise than just polynomial/non-polynomial. In this context, I saw for example the cell-probe model used.

If you care about correctness, then still other models are useful. Here you have operational semantics (which I'd say is the analogue of lambda calculus for statefull computations), axiomatic semantics (developed in 1969 by Hoare based on Floyd's inductive assertions from 1967, which are popularized by Knuth in The Art of Computer Programming, volume 1), and others.

To summarize, I think you are after models of computation. There are many such models, developed with various goals in minds, and many have state, so they correspond to imperative programming. If you want to know if something can be computed, then look at Turing machines. If you care about efficiency look at RAM models. If you care about correctness look at models that end in "semantics", such as operational semantics.

Finally, let me mention that there is a big book online only about Models of Computation by John Savage. It is mostly about efficiency. For the correctness part I recommend you start with the classic papers of Floyd (1967), Hoare (1969), Dijkstra (1975), and Plotkin (1981). They are all pretty cool.