H.K. Hung and J.I. Zucker (1991): Semantics of pointers, referencing and dereferencing with intensional logic, in Proceedings of Sixth Annual IEEE Symposium on Logic in Computer Science, Amsterdam, July 1991, 127-136. [text.ps]

Abstract. We apply intensional logic to the semantics of an Algol-like programming language. This 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 great advantage of this approach is that it preserves compositionality of the meaning function, even in "opaque contexts".

Earlier work in this direction, by Janssen and Van Emde Boas, dealt with the semantics of assignments to simple and indexed variables and pointers, without, however, considering "dereferenced" pointers on on the left or right hand side of assignments. More recent work by Hung applied this approach to to the semantics of blocks and procedures with parameters (passed by value, by reference and by name).

The present work extends this approach 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.