March 5th, 2003

beartato phd

(no subject)

The apparent recent result of the undecidability of higher-order beta matching surprised me much less after i realized it didn't cover beta-eta. Still a neat result. It makes me feel pessimistic about the beta-eta problem, though, which is sad.

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.