Standard ML-NJ weak polymorphism and imperative constructs

Abstract
Standard ML of New Jersey (SML-NJ) uses "weak type variables" to restrict the polymorphic use of functions that may allocate reference cells, manipulate continuations, or use exceptions. However, the type system used in the SML-NJ compiler has not been presented in a form other than source code and has not been proved correct. We present a type system, in the form of typing rules and an equivalent algorithm, that appears to subsume the implemented algorithm. Both use type variables of only a...

This publication has 8 references indexed in Scilit: