For students taking 6.888 that are interested in learning Coq over IAP, here's our current plan (be sure to see the initial "homework" assignment in step 2):
You will work through select chapters from Pierce's Software Foundations online book.
In particular, the plan is to focus on the Imp and Hoare chapters, with some possible follow-on directions (proof automation, code extraction) that we will describe on the first day (Jan 26th).
The path through the chapters you should do is, in order:
If you are not familiar with Coq already, you should start by working on the above chapters, at least through MoreLogic. Make sure you actually do all of the exercises! This can take a significant amount of time, depending on your background, but it will be HUGELY useful in anything you will do later on in Coq.
On the first day of the IAP class, we will discuss any exercises that you had trouble with in Preface through MoreLogic, and we will start working through Imp and Hoare.
We will meet every day, Jan 26-30, in the 32-G9 lounge outside of the elevators, starting at 11am, and going on until ~3pm or whenever you all decide to leave. We don't plan to lecture almost at all; the focus will be on helping you work through the Software Foundations exercises and follow-on ideas, and on answering any questions about the material.
We will provide LUNCH every day that week (around noon), to get you to come!
If you have any questions, send email to 6888-staff@csail.mit.edu.
The IAP class is not offered for credit, and does not have a subject number.