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.