Welcome to the EECS 755 blog for Spring 2020. You will find late-breaking information about the class and associated projects and exams here. The blog is available via RSS feed if you use an RSS aggregator.
As you’re getting started it would be a good idea to installed Coq on your system of choice. If you are not an emacs and linux user, it is strongly suggested that you use CoqIDE to get started. Is the name implies it provides a drag-and-drop installation as well as a graphic interface for Coq. Should you become a power user, you will eventually want to move to emacs and ProofGeneral.
Before starting anything else, get Coq installed and running on a machine you have access to. There are many ways to do this (see the homepage for a few). The easiest way to do this is install the Coq IDE, but the best ways are using emacs or VSCode as a frontend. Coq must installed before proceeding.
I will be assigning problems from Adam Chlipala’s Formal Reasoning About Programs (FRAP) text referenced on our class homepage. The problem sets and a bunch of support files including the text are available via a github repo at:
When you do your clone of this repo, use the
recursive option to
install the FRAP book and libraries:
git clone --recursive firstname.lastname@example.org:mit-frap/spring21.git
In the resulting repo you will find a directory
frap that contains
Frap.v library, the FRAP text, and acompanying FRAP Coq
files. Descend into this directory and run
make to build the book
and libraries. The build takes awhile, so be patient.
You will also find a
README.md file in the base directory that contains
instructions for using the problem sets.g If you don’t install and
frap submodule above, none of the problem sets will work
I will go through most of this in class, but please try to get Coq and the problem sets installed on your own. It’s helpful to have tried all this once before you see it live.