Lambda, the ultimate TA: using a proof assistant to teach programming language foundations

Abstract

Ambitious experiments using proof assistants for programming language research and teaching are all the rage. In this talk, I'll report on one now underway at the University of Pennsylvania and several other sites: a one-semester graduate course in the theory of programming languages presented entirely - every lecture, every homework assignment - in Coq. I'll try to give a sense of what the course is like for both instructors and students, describe some of the most interesting challenges in developing it, and explain why I now believe such machine-assisted courses are the way of the future.