I will overview bisimulation techniques in higher-order languages (lambda-calculus like, possibly enriched with imperative features such as references) and then discuss the addition of (discrete) probabilities.