Advisor meeting was brief, because Frank had some grading to do. Discussed some hazy blue-sky ideas about frameworks and contexts and modalities and stuff. I think maybe dependency might still somehow be sneakable in to even "non-flat" context logics like bunched, non-associative, etc.
More stuff to read: pure type systems semantics, something with links to an explicit substitution calculus I haven't heard of. Looks as if this is the canonical paper.
You know what I'd like? If middle-clicking in a text field on mozilla (either (a) with some modifier key or preceding keystrokes or (b) whenever the clipboard has the prefix "http://") pasted <A HREF="contents of clipboard go here"></A> and left the cursor just before the close-tag. I wonder if that's easily hackable.