@INPROCEEDINGS{PittsAM:evall,
AUTHOR={A.~M.~Pitts},
TITLE={Evaluation Logic},
BOOKTITLE={IVth Higher Order Workshop, {Banff} 1990},
SERIES={Workshops in Computing},
EDITOR={G.~Birtwistle},
PUBLISHER={Springer-Verlag, Berlin},
YEAR=1991,
PAGES={162--189},
ABSTRACT={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 {\em Natural
Semantics\/} style of structural operational semantics~\cite{Kah}.
The logic's underlying type system is Moggi's {\em computational
metalanguage}~\cite{Mog1}, 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
{\em evaluation modalities}. The categorical structure corresponding
to this kind of logic is explained and a couple of examples of
categorical models given.\par
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~\cite{MTH}. 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.}}