The proof script is availabele for download (2009-6-15). It is part of my masters thesis, hence it includes quite some document markup and may still be subject to change.
The finished thesis can be obtained here
In informal proofs one tends to identify terms up to alpha equivalence, but issues arising from this identification are usually glossed over. Compared to informal proofs, these issues make formal proofs about calculi with binders rather tedious.
Nominal Logic as implemented in Isabelle/HOL-Nominal is one approach to facilitate formal reasoning about names and binders.
The original idea was to formalize the strong normalization proof of Levy's call-by-push-value calculus which I have done in my Bachelor's Thesis the basic proof technique to prove strong normalization of CBPV was TT-lifting as introduced by Pitts and Stark to prove strong normalization of Moggi's computational metalanguage.
Since cbpv is a considerable extension of the computational metalanguage I started by formalizing their proof in Isabelle/HOL-Nominal which already revealed numerous interesting issues.
I gave my first talk for my Master Seminar on the theoretical background underlying the Nominal Package I use to formalize TT-lifting. The slides can be found here
I gave a second talk on the issues I encountered while formalizing TT-lifting. The slides of this talk can be downloaded here
The final talk for my Master's thesis can be obtained here.