Inside 206-105

Existential Pontification and Generalized Abstract Digressions

November, 2010

My first proof in Isabelle

One of the distinctive differences between academic institutions in the United States and in Great Britain is the supplementary learning outside of lectures. We have recitations in the US, which are something like extra lectures, while in the UK they have tutorials, or supervisions as they are called in Cambridge parlance. As always, they are […]

Reflexivity. Qed.

In which Mendeley, Software Foundations and Coq are discussed. I was grousing on #haskell-blah one day about how annoying it was to organize all of the papers that I have downloaded (and, of course, not read yet.) When you download a paper off the Internet, it will be named all sorts of tremendously unhelpful things […]

Integer sequences every computer scientist should know?

The On-Line Encyclopedia of Integer Sequences is quite a nifty website. Suppose that you’re solving a problem, and you come up with the following sequence of integers: 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2... and you wonder to yourself: “huh, what’s that sequence?” Well, just type it in and the […]

Is multiply-carry strongly universal?

I’ve been wanting to implement a count-min sketch for some time now; it’s a little less widely known than the bloom filter, a closely related sketch data structure (that is, a probabilistic data structure that approximates answers to certain queries), but it seems like a pretty practical structure and has been used in some interesting […]

Cambridge potpourri

In which Edward tells some stories about Cambridge and posts lots of pictures. Apparently, Alyssa B. Hacker (sic) went on the Cambridge-MIT exchange. This is perhaps a phenomenon of having been around MIT for too long, a campus which has a reputation for not being too picturesque (I can probably count the actually pretty spots […] committee

Ever try to go to and notice that it was down? Well, now you have someone to complain to: the committee has formed and apparently I’m on it. 8-) One of the first things we’ll be doing is moving from a server being hosted at Yale (the hosting has been good, but […]

It’s just a longjmp to the left

And then a signal to the ri-i-i-ight. One notable wart with readline is that if you ^C during the prompt, nothing happens, and if you do a second ^C (and weren’t buggering around with the signal handlers) your entire program unceremoniously terminates. That’s not very nice! Fortunately, readline appears to be one of the rare […]

You are in a maze of twisty little passages, all alike… (a GHC hacking post)

About a month ago I decided that it would be cool if I could solve the bug GHC's runtime never terminates unused worker threads. Well, I just got around to looking at it today, and after wandering aimlessly around the twisty maze that is the GHC RTS for an hour or so, I finally found […]

mod_fcgid 2.3 is broken (fixed in 2.3.6)

This is a post to get some Google juice for a problem that basically prevented Scripts from being able to cut over from Fedora 11 to Fedora 13. The cluster of new machines kept falling over from load, and we kept scratching our heads, wondering, “Why?” Turns out, the following commit broke mod_fcgid in a […]

Medieval medicine and computers

This is a bit of a provocative post, and its impressions (I dare not promote them to the level of conclusions) should be taken with the amount of salt found in a McDonald’s Happy Meal. Essentially, I was doing some reading about medieval medicine and was struck by some of the similarities between it and […]