Looked at Rohwedder and Pfenning's "Mode and termination checking for higher-order logic programs". Things beginning to click together mentally. The deadline for the databases project proposal is sooner than I'd like. Rrg. Also: looked over Virga "Higher-Order Superposition for Dependent Types", Virga's thesis, Pientka "Termination and Reduction Checking for Higher-Order Logic Programs". This type subordination stuff finally makes sense. Pientka and Pfenning "Termination and Reduction Checking for Higher-Order Logic Programs" looks exciting - I remember Frank talking about this stuff the last couple weeks. Going to have to read it tomorrow when I'm more awake. This is good, though. I feel like the math-digesting part of my brain just woke up again during the last day or two.