I'll be giving a mini-course on proving program termination/liveness at Imperial, May 26th, 27th, and 28th, from 2-4pm. If you're in the London area you're welcome to come, to send students, etc. These lectures will be a condensed version of the 14 lectures on the same topic that I gave at Carnegie Mellon this winter, and preliminary version of what I will give at Marktoberdorf this summer.