Tomorrow, Feb 14, Vassilis will give a tutorial on Coq, a leading tool for "mechanized metatheory" amongst other things. We'll follow that up with Tea & Cookies. Cheers!