Lambda the Ultimate

Not really about PLT, but this paper was mentioned on LtU before, and I believe it is a good reminder to people thinking that "research" means "useless".

Rigour is good for you and feasible: reflections on formal treatments of C and UDP sockets

Language designers give rigorous specifications of language syntax as a matter of course. [...] Rigorous definitions of type systems is less common [...] The situation for behavioural specification is even worse. [...] In the long term, we believe greater rigour is essential in the development of more robust software at all levels; there are many behaviourally subtle aspects of operating systems which could benefit from it, and for which the tools are now available.

Testimonials :-) :

"It would be difficult indeed to get more hard-nosedly pragmatic than C and sockets."
-- Paul Snively