Week

Topic

Work

1

Introduction and Overview

• Read: The Golden Age of PL Research

• Survey: Getting to know you

2

Coq Basics

• Read: LF Basics, Induction, & Lists

3

Basic Mechanics of Operational Semantics

• Slides: PLMW 2020

• Read: Type Safety in Three Easy Lemmas

• Read: LF Poly, Tactics

4

Mechanizing Basic Mechanics

• Read: LF Logic, IndProp Maps