  We describe an alternative approach to handling mutable references (aka.
pointers) within a gradually typed language that has different efficiency
characteristics than the prior approach of Herman et al. [2010]. In particular,
we reduce the costs of reading and writing through references in statically
typed regions of code. We reduce the costs to be the same as they would in a
statically typed language, that is, simply the cost of a load or store
instruction (for primitive data types). This reduction in cost is especially
important for programmers who would like to use gradual typing to facilitate
transitioning from a dynamically-typed prototype of an algorithm to a
statically-typed, high-performance implementation. The programmers we have in
mind are scientists and engineers who currently prototype in Matlab and then
manually translate their algorithms into Fortran. We present the static and
dynamic semantics for mutable references and a mechanized proof of type safety
using the Isabelle proof assistant.
