August 12th, 2003

beartato phd

(no subject)

So earlier today I just casually popped into the lounge and pointed out to dan that if he could score some other players I would be up for boggle. I didn't really think he would succeed (not today anyway) but to my surprise I heard a rap, rap, rapping at my chamber door roundabout 23:00, from dan, ellen, and lacey. A bit of pleasant boggling ensued, and then we were off the F&F to celebrate ellen's birthday; I think now that she had earlier forgot that she was planning the midnight-just-beginning-the-day-of timing, but I had forgot. Good thing I got roped in so fortuitously!

So a while ago I believed I really didn't like fuel and fuddle, but I gave them another earnest try tonight, attempting the pizza again. It still tastes a little... I don't know, kind of a burnt flavor without actually being burnt. Still okay, though. Just not something I would prioritize eating. I still owe them another chance or two before I really give up.

And... oh, dear.

LiveJournal Haiku!
Your name:jcreed
Your haiku:a dream in the grad
cs lounge hacking on research
nothing like a girl
Created by Grahame
beartato phd

(no subject)

Dreams: one, involving believing that lars_chan had a great-uncle by the name of David Semesky who was giving me advice on something or other. Two: good ol'-fashioned flying dream. I love flying dreams.

Woke up, and worked out, at last, I think, how to do the translation from LF to LF*. At first I thought that I'd have to actually define a function whose domain was typing derivations, yecch. I hate trying to work out the syntax of that, involving huge \left(s and \right)s around prooftree environments. Fortunately, I think I know how to avoid that now, though my first attempt got pretty far before I realized I needed more type information around, and that doomed that.

Man, dependent type theories are like rampantly incestual families, I tell you. Terms gettin' with types, types gettin' with terms... A fella cain't hardly sort it all out.
beartato phd

(no subject)

Hacking away on this proof here. I'm really excited that I think I see all the machinery coming together. It's kind of strange, that there's this one argument that seems necessary that feels very... I don't know, mechanical, in the hazy-mathematical-analogy kind of way, that there are all of these requirements and hypotheses and inferences all buzzing around doing just the right things to each other, and yet, in the implementation, it translates to zero code. It feels so much, to my intuition, like the execution of a program, but it is just a pile of logical dominos that intstantaneously fall, and imply that the program can just go on its merry way and be sure that it is correct at a certain point.

Around 9ish arilinn borrowed lincoln3's PS2 since he's out of town, and then techstep, gopi, and I went out for taco bell and krispy kreme. Yum.

This means I still have 10 original glazed that need eating if any of y'all reading feel social and jonesing for sugar tomorrow.