*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.*