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.