Logic in Computer Science (LICS 1993)

Paper: Standard ML-NJ weak polymorphism and imperative constructs (at LICS 1993)

Authors: My Hoang John Mitchell Ramesh Viswanathan

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. A type system, in the form of typing rules and an equivalent algorithm, that appears to subsume the implemented algorithm is presented. Both use type variables of only a slightly more general nature than the compiler. One insight in the analysis is that the indexed type of a free variable is used in two ways, once in describing the applicative behavior of the variable itself and once in describing the larger term containing the variable. Taking this into account, an application rule that is more general than SML-NJ is formulated for applications of polymorphic functions to imperative arguments. The soundness of the type system is proved for imperative code using operational semantics

BibTeX

  @InProceedings{HoangMitchellViswan-StandardMLNJweakpol,
    author = 	 {My Hoang and John Mitchell and Ramesh Viswanathan},
    title = 	 {Standard ML-NJ weak polymorphism and imperative constructs},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1993},
    year =	 1993,
    editor =	 {Moshe Vardi},
    month =	 {June}, 
    pages =      {15--25},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }