" /> Ezra's Research: April 2008 Archives

« March 2008 | Main | August 2008 »

April 24, 2008

Mitzenmacher's Theory Book

I like this vision Michael Miztenmacher is promoting for a book aimed at high school sophomores that explains well-understood topics in theoretical CS and describes a big open problem in each area. Besides getting the word out about the great ideas we have, it could stir enthusiasm through the big looming problems.

When I was around that age, I gorged myself on A. K. Dewdney's The Turing Omnibus: 61 Excursions in Computer Science (now 66), which treats a variety of topics very readably. It rotates around: one chapter might be on some kind of automaton and the next on an AI technique, but each area returns in time, so it develops each in chewable doses.

null == undefined

(Salad with) Steve Jenson lays it down for you: the null vs. undefined nonsense in JavaScript. Better recognize.

April 14, 2008

Yhc : Haskell -> JavaScript

A note on compiling Haskell to JavaScript, and interfacing with the DOM, in Yhc.

April 13, 2008

A located lambda calculus

Oh right. Last week I submitted a paper to ICFP. Here it is: "A located lambda calculus," by Ezra elias kilty Cooper and Philip Wadler. The abstract:
Several recent language designs have offered a unified language for programming a distributed system; we call these “location-aware” languages. These languages provide constructs that allow the programmer to control the location (the choice of host, for example) where a piece of code should run, which can be useful for security or performance reasons. On the other hand, a central mantra of web engineering insists that web servers should be “stateless”: that no “session state” should be maintained on behalf of individual clients—that is, no state that pertains to the particular point of the interaction at which a client program resides. Thus far, most implementations of unified location-aware languages have ignored this precept, usually keeping a process for each client running on the server, or otherwise storing state information in memory. We show how to implement a location-aware language on top of the stateless-server model.

April 3, 2008


It's customary to indicate the end of a proof with a little square (a "tombstone"), with "Q.E.D.," or elsewise. These marks almost never seem helpful to me, but there are other points where significant proof obligations are discharge, and I wish these were marked.

One instance is the end of a case, in a proof by cases. Each of these is a major branch of the proof, which dead-ends in the middle. Variables may be brought into scope, which evaporate when the case is completed, so it's important to know the bounds of that case.

My contribution, then, to the technique of proof-by-cases, is to introduce the marker "huzzah!" indicating the simple end of a case as well as one's excitement at having proven something—a miminal proof-unit, perhaps. Here it is in a screenshot:

Having trouble achieving this effect yourself? Here's a TeX macro:


Update: According to Wikipedia, "Paul Sally at the University of Chicago is known for ending proofs with a pirate face symbol." This doesn't seem to be true of the couple of books coauthored by Sally that I could get through Google Books.