CSE 505 Autumn 2016

Overview

We'll study techniques for thinking crisply about programming languages, write some fascinating programs, and discuss various design tradeoffs. We will roughly follow Dan Grossman's traditional 505 material using the Coq proof assistant.

Meeting	Mon, Wed 9:30 ARC G070
Instructor	Zach Tatlock (ztatlock@cs)
	Thu 9:30 CSE 546
TA	Konstantin Weitz (weitzkon@cs)
	Tue 9:30 CSE 218
Tutor	James Wilcox (jrw12@cs)
	Fri 13:30 CSE 674
Tutor	Eric Mullen (emullen@cs)
	Fri 13:30 CSE 674
Tutor	Joe Redmon (pjreddie@cs)
	Fri 13:30 CSE 674
Discussion	Piazza
Syllabus	Calendar
Scores	505 Gradebook

Lectures

Discussions

We'll read and discuss a handful of papers this quarter. Most of the readings are relatively non-technical; they're intended to foster discussion and debate. By noon the day before each discussion, please submit a short review. Your review should have three small paragraphs: (1) a high-level summary of the paper and a concise recap of its main take-away; (2) a description of what you most valued learning from the paper and what the paper's greatest strengths are; and (3) a discussion of what you disagreed with or felt could be improved to make the paper stronger.

Please submit your reviews in plain text format , in a single file, including only ASCII characters (no Unicode please), using the .txt file extension, via the 505 Dropbox. (Please note, this means you should NOT submit a PDF!)

Problem Sets

Please work on your problem sets with a partner. It should be more fun and help you meet folks in the department you may not have otherwise gotten a chance to work with. To find a partner who is not in your lab, try the Piazza partner search. Also, make sure to work with a different partner for each problem set. Only one member of each team should submit a solution. Please clearly indicate both team members in a comment at the top of your submission. Happy hacking :)

Also, make sure to check out Joe's tactic index to get up to speed with Coq tactics and see what's available!

Submit problem sets via the 505 Dropbox. If you absolutely must, you can submit up to 2 days late, but the policy is to subtract 10% per day.

Exams

Unlike problem sets, exams should be entirely your own work. Please submit your exam via the 505 Dropbox.

Help

You can always get help on Piazza, but nothing beats a genuine face-to-face meeting.

If you'd like to interact with a real person please come to Zach's office hours (Thu 9:30 CSE 546), Konne's office hours (Tue 9:30 CSE 218), or drop in on the Coq Tutoring sessions (Fri 1:30 CSE 674). Because schedules are hectic, some times and locations may change throughout the quarter, so we've included the exact schedule for in-person help below:

More

Setting up Coq

This course will use CoqIDE 8.5pl2 and OCaml 4.02 or later. We have provided a VM with all the required software, or you can set up your own machine.

Using the provided VM.

To use the CSE 505 VM please download it and run with VirtualBox.
You will also need to install the menhir package which we missed when setting up the VM. To install menhir, open a terminal and type:
```
sudo apt-get install menhir
          
```
(Thanks to Everett Maus for pointing this out!)

Setting up an Ubuntu machine.

You first have to install Ocaml. To do so, open a terminal and type:

apt-get update && apt-get install -y \
  camlp5 \
  libpcre-ocaml-dev \
  libpcre3-dev \
  pkg-config \
  liblablgtksourceview2-ocaml-dev

Then install Coq with:

curl -O https://coq.inria.fr/distrib/8.5pl2/files/coq-8.5pl2.tar.gz
tar -xvf coq-*.tar.gz
cd coq-*
./configure \
  -bindir /usr/local/bin \
  -libdir /usr/local/lib/coq \
  -configdir /etc/xdg/coq \
  -datadir /usr/local/share/coq \
  -mandir /usr/local/share/man \
  -docdir /usr/local/share/doc/coq \
  -emacs /usr/local/share/emacs/site-lisp \
  -coqdocdir /usr/local/share/texmf/tex/latex/misc
make; sudo make install

You can test your setup by running the following commands. (Each command starts with a $, which you should not enter into the terminal. The expected output of each command is shown on the next line.)
```
$ ocaml -version
The OCaml toplevel, version 4.02.3

$ coqc --version
The Coq Proof Assistant, version 8.5pl2 (September 2016)

$ coqide
```

Setting up an OS X machine.

Get the CoqIDE 8.5pl2 DMG. Double click it and drag CoqIDE into Applications. Test that you can open CoqIDE by finding it in Applications and double clicking it. You should see something like this:
In order to build Coq projects from the command line (recommended), you need to add /Applications/CoqIDE_8.5pl2.app/Contents/Resources/bin to your PATH. You can do this by adding the line
```
export PATH=/Applications/CoqIDE_8.5pl2.app/Contents/Resources/bin:$PATH
```
to your ~/.bashrc file. Create that file if it does not already exist. Also, add the following lines to ~/.bash_profile if they are not already there in order to activate your ~/.bashrc file.
```
if [ -f ~/.bashrc ]; then
    source ~/.bashrc
fi
```
To test, open a new terminal and type coqc --version. You should see something like this:
```
The Coq Proof Assistant, version 8.5pl2 (July 2016)
compiled on Jul 8 2016 13:35:37 with OCaml 4.02.3
```
Install the homebrew package manager, if you haven't already.
Use homebrew to install OCaml, OCamlbuild and Menhir by saying
```
brew install ocaml ocamlbuild menhir
```
This command may take some time (5 minutes) to complete and is a good opportunity to go to the PLSE lab (CSE 407) and enjoy the free coffee/tea and company!
You can test your OCaml setup by running the following commands. (Each command starts with a $, which you should not enter into the terminal. The expected output of each command is shown on the next line.)
```
$ ocaml -version
The OCaml toplevel, version 4.03.0

$ ocamlbuild -version
ocamlbuild 0.9.2

$ menhir --version
menhir, version 20160526
```
You're all set! Go prove some theorems!

Resources

Joe is leading the development of a new tactic index to help you learn what Coq tactics are available and how they work. Check it out and send us feedback!

Pierce's superb Software Foundations is very closely related to our course.

Chlipala's excellent Certified Programming with Dependent Types is great for continuing to develop more advanced Coq hacking skills.

The classic 505 materials and Types and Programming Language textbook are also excellent for learning all the material we'll cover in class and more, but from a traditional pen-and-paper perspective.

For some notes on bullets in proof scripts, see "Structuring proofs with bullets" and the Coq manual on bullets.

CSE 505: Programming Languages