gistfile1.txt

Take the following countable signature:

true
false
undefined
null
ref1, ref2, ..., refN, ...
str1, str2, ..., strN, ...
pair(x, y)
object(x, y)
function(x, y)

Then take all ground terms of this signature. A subset of those are said to be wellformed if they are in the domain of "typeof" defined as follows:

typeof(undefined) = Undefined 
typeof(null) = Null
typeof(true) = Boolean
typeof(false) = Boolean
typeof(object(ref_i, Y)) = Object if Y is a mapping term.
typeof(function(X, str_i)) = Function if X is a mapping term.

We say that X is a mapping term iff X is either null or is pair(pair(str_i, ref_j), Y) for some i, j and a mapping term Y.

We can also defined auxiliary mapping refs : dom typeof -> 2^{ref_i} in a straightforward way: for every term its a set of ref_i that occur inside it.

Now if we take dom typeof we have ability to describe a state of JavaScript execution as a function S : { ref_i } -> dom typeof, such that

forall ref in dom S : S(ref) subseteq dom S and if for some X . S(ref) = object(proto, X) then typeof(S(proto)) = Object.