The Penn PL Club is presenting a Coq tutorial at POPL 2008. It covers Coq basics, the simply-typed lambda calculus, and System F<:. If you can’t attend, you can download the code, which is intended to be self-contained and looks quite clear.
Twelf is a language based on the LF logical framework and can be used for specifying the metatheory of logics and programming languages. It includes a theorem prover and a theorem checker.
Here are some resources on Twelf: Andrew Appel’s tutorial, John Boyland’s tutorial, and Mechanizing Metatheory in a Logical Framework, by Robert Harper and Dan Licata, to appear in JFP.
