In this paper we study polyplain , a Church-style typed lambda
calculus with impredicative polymorphism and mutable references.  We
formalize the syntax, type system and call-by-value operational
semantics for polyplain in the Isabelle/HOL theorem prover and prove
the type safety of the language.