We describe a simple denotational semantics, using possible worlds, for a call-by-value language with ML-like storage facilities, allowing the storage of values of any type, and the generation of new storage cells. We first present a criticism of traditional Strachey semantics for such a language: that it requires us to specify what happens when we read non-existent cells. We then obtain our model by modifying the Strachey semantics to avoid this problem. We describe our model in 3 stages: first no storage of functions or recursion (but allowing storage of cells), then we add recursion, and finally we allow storage of functions. We discuss similarities and differences between our model and Moggi's model of ground store. A significant difference is that our model does not use monadic decomposition of the function type.
展开▼
