[ 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
