interest is in stating and proving metatheorems on completeness, decidabil-
ity etc. Such aims are best served with logics with a limited expressivity, as
increase in expressivity generally leads to loss of metalogical properties. On
the other hand, the goal of providing a general logical framework for program
semantics, as we find it in denotational semantics, does not square well with
such limited expressivity. In this area and for this purpose we must have
rich and typed logics. Our decision to use classically typed models instead
of the domains one usually finds in denotational semantics brings us closer
to the dynamic enterprise, but we still need a logic which is more expressive
than the ones which are characteristically studied in that tradition. The
goals and aims of Dynamic Semantics and Denotational Semantics are of a
complementary rather than of an opposing nature and in fact the present
logic can be viewed as a typed extension of Quantificational Dynamic Logic
(QDL): see [14, 17] for an embedding of QDL into (a variant of) the present
system which is related to the well-known embedding of PDL into Lω1ω .
Giving the semantics of a language by means of a compositional trans-
lation into some typed logic is a procedure which is known in linguistics
under the name of Montague Semantics [11, 12]. Linguists try to explain
the semantics of, say, English by translating fragments of that language into
suitable higher-order logics. We do the same here for a simple programming
language, thereby threading into the footsteps of Janssen [10], who gave a
Montague Semantics for programming by translating fragments of an Algol-
like language into a special Dynamic Intensional Logic. Janssen did not give
a treatment of recursion and we hope to improve upon his work by repair-
ing this omission. Janssen’s logic has also played a role in linguistics, as
Groenendijk and Stokhof have applied it to this area with some success in
[6]. Variants of the axiomatic extension of classical logic that will be used
in this paper have been used by the present author for giving the semantics
of fragments of English in [14, 15, 16] ([14] also considers a treatment of the
while languages). A related system, which uses a non-classical set-up, is Van
Eijck’s interesting paper [26]. Van Eijck prefers to replace the non-logical ax-
ioms of [14] by certain extralogical requirements on his models, but proves
that some important properties of standard logic are not lost.
The set-up of the rest of this paper is as follows. In section 2 we shall
define a simple programming language with choice and recursion, give some
abbreviations and introduce some necessary syntactic conventions. In sec-
tion 3 then, we present a calculus C in which certain rewriting operations
on programs are possible. These rewritings are in close correspondence to