Spent a lot of time in the library today and yesterday dereferencing pointers. I found a good survey paper [Klop 1990] on term and abstract rewriting systems, a couple proofs of Newman's Lemma (Weakly confluent and strongly normalizing imply confluent) by Huet and Barendregt and read Huet's original unification paper.

Read 158 pages of someone else's copy of Microserfs. Amusing. I should finish it some time.