Induction and logical relations September 18, 2013
Logical relations are a proof technique which allow you to prove things such as normalization (all programs terminate) and program equivalence (these two programs are observationally equivalent under all program contexts). If you haven’t ever encountered these before, I highly recommend Amal Ahmed’s OPLSS lectures on the subject; you can find videos and notes from yours truly. (You should also be able to access her lectures from previous years.) This post is an excuse to talk about a formalization of two logical relations proofs in Agda I worked on during OPLSS and the weeks afterwards. I’m not going to walk through the code, but I do want expand on two points about logical relations: