Coq for POPL folkUsing Proof Assistants for Programming Language Research or, How to write your next POPL paper in Coq San Francisco, CA January 8th, 2008 A tutorial on the use of the Coq proof assistant in formalizing programming language metatheory. This tutorial will be tailored to people who are familiar with syntactic proofs of programming language metatheory, such as type soundness, but have never used a pro
