CSC 530, Fall 2024🔗

Schedule/Homeworks Listed Here

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🔗

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🔗

• Prabakhar Ragde, "Logic and Computation Intertwined"

• Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, and Jannis Limperg, "The Hitchhiker’s Guide to Logical Verification (2024 Edition)"

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 Exams🔗

There will be no exams in this class.

10 Grades🔗

Grades will be determined by your performance on programming projects, and your class interaction.

• Assignments: 40%

• Class Participation: 60%

11 Schedule/Homeworks🔗

Here is the link again.