From Semantics to Types: the Case of the Imperative lambda-Calculus