  Reference immutability is a type based technique for taming mutation that has
long been studied in the context of object-oriented languages, like Java.
Recently, though, languages like Scala have blurred the lines between
functional programming languages and object oriented programming languages. We
explore how reference immutability interacts with features commonly found in
these hybrid languages, in particular with higher-order functions --
polymorphism -- and subtyping. We construct a calculus System F-sub-M which
encodes a reference immutability system as a simple extension of F-sub and
prove that it satisfies the standard soundness and immutability safety
properties.
