Abstract: Many POPL folks are using computer proof assistants these days, and more or less all of them are feeling the pain of writing and maintaining detailed manual proof scripts. In this tutorial, I will give a taste of how to skip the pain by writing highly automated proof scripts in Coq. These scripts in a sense explain why a theorem is true at a high level rather than giving the nitty-gritty details, which often allows a single script to be used through multiple evolutions of a theorem. Examples will be drawn from semantics of programming languages and compiler verification. No prior Coq experience will be assumed, though familiarity with the basics of programming language semantics will be helpful.
Learning objectives: Participants should come away able to write simple Coq proof scripts that adapt automatically as new cases are added to the syntax and semantics of programming languages.