Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
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.
You might want to look at chapters 13 and 19 of Types and Programing Languages that handle types for constructs with side-effects, and a more general imperative language (Java) respectively.
As Andrej says, the type system community is aware of imperative languages (indeed, I know of very few completely pure systems!), and theory has developed accordingly.
I don't know much, but I am pretty sure Linear Type Theory is used to model imperative programs. For example, Adoption and focus: practical linear types for imperative programming or On linear types and imperative update. Rust, for example, is built on something related to linear types (I forget what exactly though).
It appears the more general category of type systems is Substructural type systems. Here is some more good info on that.
