Banning Elsevier, scientists of the world, unite!

Teaching Semantics with a Proof Assistant: No more LSD Trip Proofs (PDF), by Tobias Nipkow. “We describe a course on the semantics of a simple imperative programming language and on applications to compilers, type systems, static analyses and Hoare logic.”

Euclidean and non-Euclidean algebra (PDF), talk by Vaughan Pratt.

The TeX Hierarchy (PDF), by Donald Arseneau, Raymond Chen, and Victor Eijkhout.

MH-V, an exmh-like interface for MH/nmh mail with GTK+ colors and Vim key bindings.

Scaling GitHub, slides by Zach Holman.

How Not To Sort By Average Rating, by Evan Miller.

RFC for the 7XX Range of HTTP Status codes: Developer Errors

The Nomad’s Ger, Mongolia’s instant house.

Test your vocab, how many words do you know?

Cumming soon: the Fleshlight iPad case, NSFW.

Complexity class or experimental drug?

Snowdecahedrons

Request for Startups 9: Kill Hollywood at Y Combinator.

Regular Expression Matching with a Trigram Index, or: How Google Code Search Worked. By Russ Cox. The trigram index is a lovely idea.

Idris is a general purpose pure functional programming language with dependent types. It is compiled, with eager evaluation.

Doozer is a highly-available, completely consistent store for small amounts of extremely important data. When the data changes, it can notify connected clients immediately.

Vacietis is a C to Common Lisp compiler inspired by the Zeta-C compiler for Lisp Machines and TCC. Very early.

Elsevier – my part in its downfall, by Tim Gower. “Why do any of us publish papers in Elsevier journals?”

A puzzle about typing, by Andrej Bauer.

Type held in the hand, stunning details of real world typesetting.

We Are Not The Dead, soldiers’ faces before, during and after serving in Afghanistan.

Piss, short movie by Bette Bentley and Vincent Peone. NSFW. “What a refreshingly honest look at the confusing world of negotiation, consent, kink and love.”

When Zombies Attack!: Mathematical Modelling of an Outbreak of Zombie Infection (PDF), by Philip Munz, Ioan Hudea, Joe Imad, and Robert J. Smith

CSS px is an Angular Measurement, by Sean B. Palmer. Lovely.

Awesome WM in Kindle Touch!, interesting choice.

Microsoft keeps it old-school with a pricey text adventure game

Let’s Play: Ancient Greek Punishment, flash “game”.

2011 music wrap-up, by jwz.

The New Web Typography, how about you give us proper justification and hyphenation first, before we talk about OpenType features?

You Say You Want a Devolution?, by Kurt Andersen. “For most of the last century, America’s cultural landscape—its fashion, art, music, design, entertainment—changed dramatically every 20 years or so. But these days, even as technological and scientific leaps have continued to revolutionize life, popular style has been stuck on repeat, consuming the past instead of creating the new.”

Hakim Bey: Repopulating the Temporary Autonomous Zone, “The TAZ may have remained a fringe work if it wasn’t for “cyberculture,” which proved among the more resilient memes in alternative art and culture from the mid-1980s to the mid-1990s.”

The quest for the most diminutive munitions program, RSA in three lines Perl explained. (And a shorter one.)

ijmenu is a small console-based selector. (And the rest of the page contains interesting ideas, too.)

Vac pots, probably the coolest sort of coffee gagdetry you can find.

A Time-Lapse Map of Every Nuclear Explosion Since 1945

Lana Sator explores a Russian Rocket factory

The Ever-Dymanic Tertial, so simple, so useful.

Abbey Road Crossing Webcam

Esmerelda’s Imagination, Rob Pike: “Go is a language for writing Go programs, not Java programs or Haskell programs or any other language’s programs.”

The personal computer is dead, by Jonathan Zittrain. Not a good thing, at all.

New Year’s Resolution: Full Disk Encryption on Every Computer You Own, yes please.

There is no 16-Clue Sudoku: Solving the Sudoku Minimum Number of Clues Problem, by Gary McGuire, Bastian Tugemann, and Gilles Civario. “We were granted almost four million core hours on JUGENE…”

Handbook of Floating-Point Arithmetic seems very comprehensive and detailed. A very CS-point of view of numerical analysis.

4chan and /b/: An Analysis of Anonymity and Ephemerality in a Large Online Community (PDF), by Michael S. Bernstein, Andrés Monroy-Hernández, Drew Harry, Paul André, Katrina Panovich Greg Vargas. I vastly underestimated the number of posts there.

The design and implementation of Ruby M17N, english translation.

Runit for Ruby (And Everything Else), good introduction to the runit supervisor.

gopher.el is an Emacs mode to browse Gopher.

The Shibumi set is not a single game but many games; it is the simplest of game systems. The set includes a 4x4 square board and 16 white, black and red balls.

The Physics Factbook, nice resource. How fast is a base ball again?

Development of Rheolism, a one line Tetris like game.

The Mystery of the Canadian Whiskey Fungus

Egg