Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
@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.}}