PiDP-11: Recreating the PDP-11/70 and PiDP-8/I: Recreating the PDP-8/I using a Raspberry Pi.
One Monad to Prove Them All, Functional Pearl by Jan Christiansen, Sandra Dylus, and Finn Teegen.
Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory, by Jesper Cockx and Dominique Devriese. “This paper proposes a proof-relevant framework for reasoning formally about unification in a dependently typed setting. In this framework, unification rules compute not just a unifier but also a corresponding soundness proof in the form of an equivalence between two sets of equations. By rephrasing the standard unification rules in a proof-relevant manner, they are guaranteed to preserve soundness of the theory.”
Linear Logic for Constructive Mathematics, by Mike Shulman.
The Eudora Email Client Source Code, now BSD-licensed!
Digital Mars C/C++ Compiler, open sourced and being ported to D.
Wrek is an Erlang library for concurrently executing task dependency graphs.
Playing battleships over BGP, because we can.