A Compilation Mechanized Metatheory Challenge

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

My solution

--Adam Chlipala