Polymorphic typing of variables and references

Abstract

In this article we consider the polymorphic type checking of an imperative language. Our language contains variables , first-class references (pointers), and first-class functions. Variables, as in traditional imperative languages, are implicitly dereferenced, and their addresses ( L -values) are not first-class values. Variables are easier to type check than references and, in many cases, lead to more general polymorphic types. We present a polymorphic type system for our language and prove that it is sound. Programs that use variables sometimes require weak types, as in Tofte's type system for Standard ML, but such weak types arise far less frequently with variables than with references