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.