A proof of the soundness of Tofte's imperative type discipline with respect to a structured
operational semantics is given. The presentation is based on a semantic formalism that
combines the benefits of the approaches considered by Wright and Felleisen, and by Tofte,
leading to a particularly simple proof of soundness of Tofte's type discipline.