CSC 530, Fall 2024
I’m so happy to be here with you!
This class is about some very beautiful ideas around dependent typing that are bringing theorem proving and program verification within reach for some nontrivial programs for the first time ever.
Our plan (er, such as it is), is to begin with a fairly detailed exploration of Prabakhar Ragde’s "Logic and Computation Intertwined" (freely available on the web), and then move on to a more "batteries included" theorem prover such as Coq, Agda, or Lean 4. The first portion of the course will consist of exercises and programming assignments. The second half of the course will ... probably also consist of exercises and programming assignments. We may be able to get to the point where we can prove things about programming language semantics. I’m optimistic but (hopefully) not foolishly so.
1 Outcomes
build a very simple theorem-prover,
formulate and prove simple theorems using dependent type theory, and
get started on stating and proving theorems about programming languages.
2 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.
3 Readings
4 Names, Times, Locations
4.1 Instructor
Brian Jones, btjones@calpoly.edu
John Clements, clements@calpoly.edu
4.2 Lecture & Lab
Section 01/02 (Jones/Clements):
Lecture: 0900-1100, Tu/Th, room 186-C101
5 Web Page
This is the course web page, its link is http://www.brinckerhoff.org/clements/2248-csc530.
6 Computing Environment
The first part of the course will use Racket. The second part will use Coq, Agda, or Lean 4. There might be a middle part that uses Pie.
We’ll see!
7 Communication
This class will use EdStem. This will be the principal means that I’ll use to notify you of deadlines, organizational updates, and changes to assignments. If you’re not keeping up with the group, you’re going to be missing important information.
It’s also the best way for you to direct questions to me and/or the class. Feel free to e-mail me with personal questions, but use the EdStem group as your main means of communication. It’s possible to post anonymously, if you like.
You should already have received an invitation to the EdStem group; let me know if you need an invite.
Don’t post your code or test cases to the group; anything else is fair game.
Also, please keep in mind that I (and everyone else) judge you based in part on your written communication. Spelling, complete sentences, and evidence of forethought are important in all of your posts & e-mails. One easy rule of thumb: just read over what you’ve written before clicking post or send, and imagine others in the class reading it.
8 Attendance Requirements
I do not formally state attendance requirements.
However, an outrageously large fraction of the grade depends on your class participation; if you don’t show up, you’re unlikely to get a good grade.
9 Installing the Handin Server
In order to hand in your work, you’ll need a plugin.
Choose File|Package Manager... , and enter this string (just copy it from this web page, WITHOUT ANY WHITESPACE, ESPECIALLY NOT A NEWLINE):
git://github.com/jbclements/racket-handin-client#2248-csc530
(If, after pasting this string in the box, it looks like it’s blank, it’s probably because you pasted something that ended with a newline. Don’t just paste again; hit the backspace key.)
This should chug away a bit, and then you should be able to close the window. Note that the only completion signal is that the "Close Output" button becomes enabled.
If any errors occur (it’ll say so at the end), be sure to copy the text so I can see it.
Quit and restart DrRacket.
You should now see a little "Poly" button labeled "handin". Don’t click it, yet. First you need to create an account.
Choose File|Manage CSC 530 Handin account...
Fill in your data. Use your cal poly login as your Username/ID (no @calpoly, just the login). Use "0" (zero) as the student ID#. Choose a password that you will remember. Click the "Add User" button when you’ve got that done.
Now, you should be ready to hand in.
10 Exams
There will be no exams in this class.
11 Grades
Grades will be determined by your performance on programming projects, and your class interaction.
Assignments: 40%
Class Participation: 60%