Benjamin Pierce

Picking up where Andrew Tolmach's lectures leave off (and following the second half of the Software Foundations in Coq text), my lectures will develop more advanced techniques for using a proof assistant to formalize and reason about programming languages. Topics will include formalizations of simple imperative programs, Hoare logic, lambda-calculus, and type systems.