A new typed, higher-order logic is described which appears
particularly well fitted to reasoning about forms of computation whose
operational behaviour can be specified using the *Natural
Semantics* style of structural operational semantics. The logic's
underlying type system is Moggi's *computational metalanguage*,
which enforces a distinction between computations and values via the
categorical structure of a strong monad. This is extended to a
(constructive) predicate logic with modal formulas about evaluation of
computations to values, called *evaluation modalities*. The
categorical structure corresponding to this kind of logic is explained
and a couple of examples of categorical models given.
As a first example of the naturalness and applicability of this new
logic to program semantics, we investigate the translation of a (tiny)
fragment of Standard ML into a theory over the logic, which is proved
computationally adequate for ML's Natural Semantics. Whilst it is
tiny, the ML fragment does however contain both higher-order
functional and imperative features, about which the logic allows us to
reason without having to mention global states explicitly.