Semantics of pointers, referencing and dereferencing with intensional logic

Intensional logic is applied to the semantics of an Algol-like programming language. This approach associates with expressions their senses, or meanings relative to possible worlds, here interpreted as machine states. These meanings lie in the semantic domains of a higher order typed intensional logic. The advantage of the approach is that it preserves compositionality of the meaning function, even in opaque contexts. This study extends earlier work in this direction, by T.M.V. Janssen and P. Van Emde Boas (1977), to pointers, including dereferenced pointers on both sides of assignments. It is shown how this approach gives an elegant solution to the problem of pointer semantics which is simple, compositional, and implementation independent