I might not be doomed:
- As of today, I'm finally caught up on TaPL -- that is, I have no more chapters left to read than I have days left to read them in. (Insert step-indexing joke here. Um.) I've been mostly skimming over the short implementation chapters, and I skipped the stuff about coercion semantics for subtyping and most of Chapter 21, which explains the metatheory of recursive types using coinduction, but other than that, I'm still on track to read the whole thing.
- I checked with Dan about exactly how much of Davey and Priestley he expects me to actually absorb. It turns out that he'll be happy if I can explain Knaster-Tarski. I, too, will be happy if I can do that.
- I read the first half of the Appel and McAllester "Indexed Model" paper. It makes so much more sense now than when I first tried to read it a year ago. Maybe indexed models of recursive types (as opposed to, for instance, the chapter of TaPL that I skipped) are both easier for human beings to understand and easier to mechanize from scratch! (They're not necessarily pretty, though. People use words like "infect" to describe what indices do to a model.)
- It's starting to become clear (well, less opaque, anyway) how all of these things are related.