Verifying Supercompilation in Coq

Almost in the nick of time, I managed to submit a paper to META-2010. It describes some of my recent experiments in Coq, particularly those related to supercompilation. The draft is (maybe temporarily) here. Let's hope I'll find some time to write more about it ... some day.