ezyang's blog

POPL is almost upon us!

Ott and PLT Redex are a pair of complimentary tools for the working semanticist.

MVars are an amazingly flexible synchronization primitive, which can serve as locks, one-place channels, barriers, etc. or be used to form higher-level abstractions.

One of the appealing things about GHC is that the compiler is surprisingly hackable, even when you don’t want to patch the compiler itself.

Apologies in advance: this post assumes familiarity with Rust.

GHC’s block allocator is a pretty nifty piece of low-level infrastructure.

Ubuntu continues on its rampage of breaking perfectly good software, and on my most recent upgrade to Saucy Salamander, I discovered to my dismay that my media keys (e.g. volume keys, fn (function) keys, suspend button, etc) had stopped working.

David Darais asked me to make this public service announcement: If you’re using lift, you’re doing it wrong.

Here at ICFP, sometimes the so-called “hallway track” is sometimes just as important as the ordinary track.

Logical relations are a proof technique which allow you to prove things such as normalization (all programs terminate) and program equivalence (these two programs are observationally equivalent under all program contexts).

One of the problems with academic publishing is that it’s hard to keep old papers up-to-date.

I just presented Blame Trees at the 13th Algorithms and Data Structures Symposium.

I write in from sunny Oregon, where the sun floods into your room at seven in the morning and the Oregon Programming Languages Summer School is in session.

One day, you’re strolling along fields of code, when suddenly you spot a syntax construct that you don’t understand.

I spent some of my plane ride yesterday working on Coq versions of the exercises in The HoTT book.

In what is old news by now, the folks at the Institute for Advanced Study have released Homotopy Type Theory: Univalent Foundations of Mathematics.

This Lambda the Ultimate post (dated 2010) describes a rather universal problem faced by compiler writers: how does one go about adding “extra information” (e.g. types) to an AST?

Adam Belay (of Dune fame) was recently wondering why Haskell’s MVars are so slow.

Ariel Rabkin has some code he’d like to verify, and at this year’s HotOS he appealed to participants of one “unconference” (informal breakout sessions to discuss various topics) to help him figure out what was really going on as far as formal verification…

Christopher de Sa and I have been working on a category theoretic approach to optimizing MapReduce-like pipelines.

Recursion and induction are closely related.

Having attempted to read a few textbooks on my Kindle, I have solemnly concluded that the Kindle is in fact a terrible device for reading textbooks.

I very rarely post linkspam, but given that I’ve written on the subject of anonymizing Bitcoins in the past, this link seems relevant: Zerocoin: making Bitcoin anonymous.

(Selinger) Here is a fairy tale: The evil king calls the poor shepherd and gives him these orders.

Humbly presented for your consideration: Exhibit A, an NDSEG essay that did not get accepted; Exhibit B, an NDSEG essay that did get accepted.

Last week, I made my very first submission to ICFP!

From the files of the ECMAScript TC39 proceedings Single export refers to a design pattern where a module identifier is overloaded to also represent a function or type inside the module.

From the files of the ECMAScript TC39 proceedings I want to talk about an interesting duality pointed out by Mark Miller between two otherwise different language features: weak maps and private symbols.

If you hang out long enough with a certain crowd (in my case, it was the ECMAScript TC39 committee), you will probably hear the term membrane tossed around.

Along with a Nexus 7, I also acquired a Kindle Paperwhite over winter break.

I’d like to talk about some nitty-gritty details of GHC’s thread scheduling, discovered over the course of working on stride scheduling for GHC.

So you want to make a web app.

I acquired a Google Nexus 7 (Wi-Fi only) over winter break.

Metro maps are a visual metaphor for complex, interdependent story lines developed by Dafna Shahaf.

On the prompting of Steven Hum, I’ve put some finishing touches on my Sup patchset and am “releasing” it to the world (more on what I mean by “release” shortly.)

You can.

Joe Zimmerman recently shared with me a cool new way of thinking about various encryption schemes called functional encryption.

Functions are awesome.

“Everything is a file.” [1] This was the design philosophy taken to its logical extreme in Plan 9.

I’m taking a Data Visualization course this fall, and one of our assignments was to create an interactive visualization.

October has come, and with it, another Ubuntu release (12.10).

I was wandering through the Gates building when the latest issue of the ACM XRDS, a student written magazine, caught my eye.

This post is the spiritual predecessor to Flipping Burgers in coBurger King.

This post is adapted from the talk which Deian Stefan gave for Hails at OSDI 2012.

So you’re half bored to death working on your propositional logic problem set (after all, you know what AND and OR are, being a computer scientist), and suddenly the problem set gives you a real stinker of a question: Is it true that Γ ⊢ A implies that Γ ⊢

Jon Howell dreams of a new Internet.

Caveat emptor: half-baked research ideas ahead.

There is a bit of scaffolding involved with making Core-to-Core transforming GHC plugins, so I made a little project, based off of Max Bolingbroke’s examples, which is a nice, clean template project which you can use to create your own GHC plugins.

Done.

Safe Haskell is a new language pragma for GHC which allows you to run untrusted code on top of a trusted code base.