Type theory for imperative programming languages?

The type theory that I have seen is all developed over lambda calculus, which is an inherently functional language.

Nevertheless, in practice imperative languages have type systems. Are there differences in the type theory for imperative vs functional languages?

Sure there are type systems for all sorts of programming languages, including the imperative ones. It's probably best to look at something simple first that exposes the gist of the matter. A classic is John Reynold's The essence of algol, which was quite influential historically, and develops many important ideas.

StackExchange Computer Science Q#111491, answer score: 5