J.I. Zucker and H.K. Hung (1991): Program semantics, intensional logic and compositionality, in Proceedings of the First Montreal Workshop on Programming Language Theory, April 1991, ed. M. Okada and P.J. Scott (Centre for Pattern Recognition and Machine Intelligence), 93-103. [text.ps]

Abstract. We apply intensional logic to the semantics of an Algol-like programming language. This associates with expressions their 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".

This approach has been applied in three areas:
(1) Assignments (Janssen and Van Emde Boas 1977)
(2) Blocks and procedures with parameters (passed by value, by reference and by name) (Hung 1990)
(3) Pointers (Hung and Zucker 1991)

It is shown how this approach gives an elegant semantics which is simple, compositional and implementation independent.