next up previous contents
Next: Basic defintion of locations Up: Imperative programs Previous: Imperative programs



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.

Fri May 24 19:01:27 BST 1996