Twelf
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.