[TYPES] completeness of type inference for stateful ML

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi list!

I'm looking for any pointers to proofs of (soundness and) completeness for
a type inference algorithm for ML-with-references (and the value
restriction). I'm especially interested in formal proofs.

So far, I've found some mechanised proofs about type inference algorithms
by Garrigue, by Nipkow, and by Dubois, but nothing yet that covers
imperative features like references.

Cheers,
Ramana