Type theory for imperative programming 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.