This chapter is concerned with proving equivalence of expressions in ML.  A useful way to specify and verify programs is to prove them equivalent to other, more familiar programs.  We discuss the laws of program equivalence for ML, first considering the effect-free fragment, then generalizing to account for effects.