This page describes a benchmark for mechanizing programming language metatheory in the spirit of the POPLmark Challenge. The particular example I've chosen deals with compiling a high-level lambda calculus down to a lower-level imperative language with manual memory management.
Challenge description in PDF format