Le
Qian and Goldberg approach: maintain the set of possible types a variable or stack may hold. (at line 5 top of stack has type {foo1, foo2})
A subset of StkTy is inconsistent if it contains two distinct terms such that
- one of the type terms is a primitive type (a consistent set with a primitive type term must be a singleton);
- one is [t] and the any non-array type other than object or ;
- one term is [t] the other [s] and {s, t} is inconsistent.
The universe of Le are consistent subsets of StkTy. ? denotes an inconsistent typing.
s ? t is s ? t, if s ? t is consistent and ? otherwise.