GCR decoding on the fly, “The little routine presented here is, with all due humbleness, hands down the best code I ever wrote.” Impressive.
The stack calculus, by Alberto Carraro, Thomas Ehrhard, and Antonino Salibra. “We introduce a functional calculus with simple syntax and operational semantics in which the calculi introduced so far in the Curry-Howard correspondence for Classical Logic can be faithfully encoded.”
Mtac: A Monad for Typed Tactic Programming in Coq, by Beta Ziliani et al. “We present Mtac, a lightweight but powerful extension to Coq that supports dependently-typed tactic programming. Mtac tactics have access to all the features of ordinary Coq programming, as well as a new set of typed tactical primitives.”
Debian Code Search is a search engine for source code – it searches all the open source projects which are included in the Debian archive. Currently, that includes about 18000 packages with 140 GiB of source code.
pristine-tar can regenerate a pristine upstream tarball using only a small binary delta file and a copy of the source which can be a revision control checkout.
Zerocoin: making Bitcoin anonymous, interesting.
Q^3 is a very new project using Mozilla’s Rust language and OpenGL 3.3 to create a Quake 3 like game.
Nestful is a simple Ruby HTTP/REST client with a sane API. By Alex MacCaw.
“Communicating sequential processes” implemented in Go, examples from Tony Hoare’s seminal 1978 paper.
learnfun & playfun, a general technique for automating NES games.
The 6th Underhanded C Contest is now Open
Why I’m quitting Mendeley, danah boyd tells.
15 Mid-Century Modern Dream Homes that will Kill Your Children