CSC 530, Spring 2008
 
1 Prerequisites
2 Names, Times, Locations
2.1 Instructor
2.2 Lecture & Lab
2.3 Web Page
3 Computing Environment
4 Readings
4.1 Suggested Background Reading:
4.2 Papers for Presentation:
4.2.1 Axiomatic Semantics:
4.2.2 Separation Logic:
4.2.3 Papers from the International Conference on Functional Programming (ICFP), 2006:
5 Assignments
6 Communication
7 Tools
7.1 GHC
7.2 Coq
8 Grades
Version: 3.99.0.26

CSC 530, Spring 2008

Schedule/Assignments

Proving things is important. A proof is essentially just a very detailed explanation. Logicians have spent centuries developing a framework for these explanations. However, proving things in these frameworks is incredibly tedious and error-prone. No one has the patience to read these explanations carefully. Computers would seem like the natural solution to this problem.

After about 20 years of false starts, theorem-proving is finally gaining traction, at least in specific domains. One of these domains is Programming Languages. In this course, we will be working with a particular theorem prover (Coq) to understand the power and limitations of these tools.

1 Prerequisites

This is an upper-level course in programming languages, and assumes a familiarity with the principles of programming languages, including but not limited to notions of scope, calling convention, evaluation rules, compound data, and basic typing.

Additionally, students are assumed to have a basic understanding of simple mathematics, including the basics of set theory, very simple algebra, and some experience with proofs and basic mathematical rigor.

Finally, it requires curiosity, and self-driven exploration.

2 Names, Times, Locations

2.1 Instructor

2.2 Lecture & Lab

2.3 Web Page

This is the course web page, its link is http://www.csc.calpoly.edu/~clements/csc530-sp08.

3 Computing Environment

We’ll be doing both programming and theorem-proving in this class. The programs you write can be in either Haskell or ML. I’ll provide Haskell support to those who need it (within reason, of course). The theorem-proving will be done in coq. Coq is available for most major platforms, at http://coq.inria.fr/. You’ll probably also want to use an interactive environment such as Proof General.

4 Readings

Each student will present at least one paper or book chapter. Some of these may be joint presentations.

4.1 Suggested Background Reading:

4.2 Papers for Presentation:

Not all of these will be chosen. However, I do want to cover the first two of these, in order.

4.2.1 Axiomatic Semantics:
4.2.2 Separation Logic:
4.2.3 Papers from the International Conference on Functional Programming (ICFP), 2006:

5 Assignments

To hand in assignments, we’ll use the old standby, "/usr/bin/handin". So, you’d hand in the files "ass1.hs" and "ass1.v" as Program 1 by typing

  /usr/bin/handin clements Program1 ass1.hs ass1.v

...assuming that both of these files are in the current directory. Note that for this class, handin will work only on the Linux hosts – I believe that vogon is the default choice.

6 Communication

There is a google group for the course, "csc530-sp08". You can request addition to the group at

http://groups.google.com/group/csc530-sp08/

I would strongly suggest that you join the group; this is where I will post things like "oh, by the way, this assignment is impossible unless you know ...." Also, you’re more than welcome to post questions to me and to each other here. Things like, "How the heck do I run ghc on vogon?".

7 Tools

The course requires the use of GHC (a Haskell compiler), and also Coq (a theorem-prover).

7.1 GHC

GHC is installed on Vogon. It’s available for your home machines from the GHC webpage.

7.2 Coq

Coq is already installed on vogon. You can run it from the command-line with

  coqtop

or

  coqtop.opt

Running it exclusively from the command-line is going to get old fast. You may wish instead to use the Emacs plugin, or the IDE.

To run it in emacs, add this line to your ".emacs" file:

  (load-file "/home/clements/lib/ProofGeneral-3.7/generic/proof-site.el")

There’s also an IDE available, coqIDE. This is not installed on vogon. It looks like it’s a part of the standard debian repositories, though.

8 Grades

Grades will be determined by performance on programming/proof projects, paper presentations, and class interaction. A small fraction of the grade is determined by the instructor’s whim. The breakdown of the grade is as follows: