Implementation of Univalence, by Cyril Cohen, Thierry Coquand, Simon Huber, and Anders MĂ¶rtberg. “This prototype includes a rudimentary type-checker, with Type:Type (to simplify) which takes univalence as a non interpreted constant. Univalence however has an interpretation in the cubical set model, which is used by the evaluator.” Very interesting!

A model of type theory in cubical sets (PDF), by Marc Bezem, Thierry Coquand, and Simon Huber. Foundation of above.

RSA Key Extraction via Low-Bandwidth Acoustic Cryptanalysis, by Daniel Genkin, Adi Shamir and Eran Tromer. “The attack can extract full 4096-bit RSA decryption keys from laptop computers (of various models), within an hour, using the sound generated by the computer during the decryption of some chosen ciphertexts.”

Programming a 144-computer Chip to Minimize Power, Chuck Moore’s talk at Strange Loop is up.

Digital restoration and typesetter forensics, by Brian Kernighan et al.

Vim in the hands of a Real Maniac, great talk by Damian Conway.

Moonpig: a billing system that doesn’t suck, by Mark Dominus. You’ll learn something there.

The notational conventions I adopted, and why, by Edsger W. Dijkstra. (Dot notation for application works better than I imagined.)

Gore-Tex gets made without managers (2008), “no one can tell any of the company’s 8,500 associates what to do.”

exabgp, the BGP swiss army knife of networking.