Lots of yak shaving to work around issues with iuthesis-alt.cls. One in particular is that that class overrides
\title to do gross stuff with the raw value you give it, but that gross stuff is necessary style for the final pdf. The big problem here is that that gross stuff means you can't use
\@title anywhere else like for setting the pdftitle. Originally I was using my entitlement.sty package to get my hands on the raw input to
\title; but there's a bug where entitlement.sty also overrides that macro rather than hooking it properly. Changing it to hook properly has proved surprisingly difficult, so I just inlined the relevant parts. Still ran into issues because AMSmath's
\uppercasenonmath (used by iuthesis-alt.cls) doesn't evaluate things far enough. Managed to fix it with judicious use of
Another yak shaving issue is that the final pdf must be double spaced (okay fine) but certain chunks need to be single spaced. I've been using setspace.sty to switch the line spread as appropriate, but kept running into issues where there'd be way too much spacing whenever switching the line spread. Finally dug into the source of setspace.sty to see how it works, and managed to find out where the extra spacing was coming from. Things look much better now.
In non-yakshaving work, I wrote up the section on strong normalization of type reduction. This is the easiest of the proofs, but at least I got some content written! Also, I think I did a better job of motivating why this proof matters than in my qual paper.