[TYPES] Formal proof of type-soundness for references in Coq

[mulhern]

Hi!

I've posted a formal proof in Coq of type-soundness for references at
http://www.cs.wisc.edu/~mulhern/proofs/type-soundness/references.html.

I think it might be interesting to people on the Coq list because it uses
the module system.

As far as I know, there is no other publicly available formal proof of
type-soundness for references available, so it might be interesting to
people on the types list as well.

-mulhern