i prefer pi

The mattress pad was unsalvageable, but as it turns out, I think that I sleep much better without it.

• You get home late and realize that you forgot to put your sheets into the dryer, so you sleep in your clothes under your comforter.
• You have ever used a wooden spoon as an eating utensil because all of your other dishes were dirty.
• You have ever drunk water from a bowl because all of your glasses were dirty.
• You view the fabric care instructions on your bed linens as “general guidelines” and end up melting a portion of your mattress pad.

Two (2) tours of a local organic/fair trade chocolate factory (all-you-care-to-eat)One (1) lovely young lady.

One (1) interesting / quirky part of town to explore.

Mix for six hours.

Allspice != Old Spice

Check out this excellent ad for BBC World.

Bob Dylan is officially a crotchety old man.

An observation from my friend David, who saw SOAP last night:

I can’t wait.

Let’s play a little “Good idea/Bad idea“, shall we?

I know; I know — it’s not that good, but I didn’t have that much to work with.

I want to be able to “surf” my portable media player. If a song comes up on a playlist or while shuffling, it would be great to jump to the “page” (list, really) for that song’s artist, album, or composer, or be able to view a list of other playlists where it exists. Anyone know of any memex-like portable media devices that currently support this type of navigation? Would it be of interest to anyone else?

I’d also like to be able to use tags to organize my music (useful when two artists collaborate or when you want to have composer/arranger/lyricist information in the composer field), but that doesn’t seem to be on the horizon either…

Two facts:

1. I love scholarly articles with titles that sound like they were written by a real person.
2. Two of my favorite undergrad classes were PHIL 342 (Advanced Symbolic Logic II: Modal and non-normal languages: Possibility and Paradox) and PHIL 414 (Philosophy of Language). My favorite twentieth-century philosophers are none other than Kurt Gödel and Saul Kripke.

It is with bitter tears that I weep, then, because I don’t have the time to attend this particular lecture on campus today:

WHO: Andrew W. Appel
AFFILIATION: Princeton University
TITLE: A Very Modal Model of a Modern, Major, General Type System
ABSTRACT:
Semantic approaches to machine-checkable proofs of type soundness for Proof-Carrying Code have not been easy—until now. We present a clean and powerful model of recursive and impredicatively quantified types with mutable references. Our model is less restrictive than previous models of impredicative references. We model all of the type constructors needed for typed intermediate languages and typed assembly languages for object-oriented and functional languages; our technique is applicable to any small-step semantics including lambda-calculus, labeled transition systems, and von Neumann machines. We have reduced the system to such a simple formulation that it becomes clear that what we have is a Kripke semantics of the Goedel-Loeb (GL) logic of provability. We have machine-checked proofs in Coq.