Variables (locations) are an essential ingredient of imperative
programs. These must not be confused with LEGO's variables,
because the latter cannot be accessed by syntactic means. In order to computationally
distinguish between different variables, we introduce location as a
new type isomorphic to natural numbers. By lifting the equality from nat to location, we may obtain a
decidable equality
such that two variables are different, if and only if their underlying
addresses differ.
In real programming languages, variables are used for a variety of types. A novelty of this work is that it does cater for arbitrary types expressible in a Unifying Theory of Dependent Types. In the declaration part of the program, variables must be mapped to their types. In this context, environments map variables to their sorts,
Env = [sort:location->Type]{x:location}sort x.