Lambda the Ultimate

A very interesting thesis, by Holger Gast, at
http://www-pu.informatik.uni-tuebingen.de/users/gast/tcg.html.

From the abstract :
This thesis presents a generator for type checkers. Given a description of the type system by typing rules, the generator yields a type checker that constructs proofs using the typing rules. Unlike earlier approaches, we derive suitable notions of proof and typing rule from an analysis of type systems and from corresponding constructs in mathematical proof theory. The approach thus respects the structure and intention of the typing rules, rather than expressing the rules in some pre-existing formalism.

I hope that TCG will be released soon.