Questions or comments regarding 6.826? Contact us on Piazza or send e-mail to the 6.826 staff at 6826-staff@lists.csail.mit.edu.
Software foundations is a good introductory text to using Coq. For 6.826 we will use a few chapters to get you ready for the 6.826 labs. To do these exercises, you will have to first install Coq and then download the source code for Software Foundations, which contains the Coq files for the exercises.
For this homework you should do the exercises of the Basics chapter. Do all the exercises up to but not including "3 stars (binary)", before the beginning of the next lecture.
If you are already familiar with Software Foundations, feel free to skip the Basics, Induction, and Lists homeworks. If you're bored, you can do an optional challenge assignment where you'll prove a regular expression matcher correct.
You don't have to submit your solutions and you won't be graded on them; but, if you are unfamiliar with Coq, you better do these exercises.
Questions or comments regarding 6.826? Contact us on Piazza or send e-mail to the 6.826 staff at 6826-staff@lists.csail.mit.edu.