<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
@INCOLLECTION{PittsAM:opebtp,
 AUTHOR={A.~M.~Pitts},
 TITLE={Operationally-Based Theories of Program Equivalence},
 BOOKTITLE={Semantics and Logics of Computation},
 EDITOR={P.~Dybjer and A.~M.~Pitts},
 PUBLISHER={Cambridge University Press},
 SERIES={Publications of the Newton Institute},
 YEAR=1997,
 PAGES={241--298},
 ABSTRACT={The aim of these notes is to describe some recent advances in
  verification techniques based on operational semantics. We focus
  upon properties of contextual equivalence (and of contextual
  preordering) of expressions in a simple, non-strict functional
  programming language equipped with an inductively defined notion of
  evaluation to canonical form.  The co-inductive characterisation of
  contextual equivalence in terms of bisimulations is presented. The
  use of co-induction for reasoning about recursively defined elements
  of lazy datatypes is illustrated. We give operationally-based proofs
  of the rational completeness and syntactic continuity properties of
  the contextual preorder.}
}