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?