COS 510: Programming Languages

Download the textbook and homeworks

The main course textbook, including homework files that you will be working in, is available here. Don't use the release at the Software Foundations web site because it not match exactly this course's homeworks. Although you can access everything directly through the COS510 web site, it's best to download everything at once so that you have all the files you need. To do that: Download sf.tgz, then unpack by tar xfz sf.tgz or equivalent. This should give you a directory sf containing one subdirectory for volumes 1,2,3,5: lf,plf,vfa,vc. The very first homework will be in sf/lf/Basics.v.

Install Coq

Install Coq 8.16.1 on your computer. The most straightforward way is to install the Coq Platform 2022.09.1. Use one of the "Recommended binary installers" for your own computer (Windows, macOS, or Linux).

Among the optional and extended packages, select coqide and VST (and anything they depend on).
Or you can do the "full level" plus VST, if you think you'll be a heavy user of Coq libraries, but you won't need that for COS 510.

After you install

These instructions are for the CoqIDE interactive development environment. There's also a very capable VSCode plugin, or you can use Emacs as an IDE. You can find information about how to use the VSCode plugin for COS 510 here.

You'll then run the "coqide" program. (You may use VS Code, Proof General or another IDE for Coq if you like, in which case the following instructions don't apply.)

In CoqIDE, visit the file Basics.v. (It's best to download the entire gzipped-tar-file; see above.)

At upper left in the toolbar, click the green down-arrow a few times. Each time you do, more of the file should turn green.

Navigation shortcut: When doing proofs in CoqIDE, you can use the mouse to click on the green proof-navigation arrows in the toolbar. But it's often more convenient to use keyboard shortcuts. CoqIDE comes with a silly default for the keyboard shortcuts: control-alt-downarrow, control-alt-uparrow, etc. I find that simply control-downarrow or control-uparrow is much easier. You can change this by going to the Edit/Preferences menu, click on the Shortcuts tab, and in the box marked "Modifiers for Navigation Menu", unselect all but <ctrl>.

You may have to do this in two rounds: First, set <ctrl> as an "Allowed modifier", then restart CoqIde, then set the "Modifiers for Navigation Menu", then restart CoqIde again.

In the Font tab of the Preferences, I suggest you use Lucida Sans Unicode. Some Coq scripts (though probably not the ones for this course) use Unicode characters for mathematical symbols.

CoqIDE should then remember your preferences for next time.