Xmonad in Coq: Programming a window manager in a proof assistant, by Wouter Swierstra.
Recursive types for free!, by Philip Wadler.
When is a functional program not a functional program?, by John Longley.
Constructivist and Structuralist Foundations: Bishop’s and Lawvere’s Theories of Sets, by Erik Palmgren.
Predicative and Impredicative Definitions
The Raster Tragedy at Low-Resolution Revisited: Opportunities and Challenges beyond “Delta-Hinting”, by Beat Stamm.
How Emacs changed my Life, slides by matz.
CPU DB, a complete database of processors for researchers and hobbyists alike.
The Elian Script, “An alternative writing system whose properties combine the linearity of spelling with the free-form nature of drawing.”
Copyright stagnation, this needs to be fixed.