In CS 245E, I will offer an alternative approach to the standard CS 245 curriculum. It will not be just a regular offering with additional topics. You will use the Racket programming language to build small proof assistants that allow human interaction in order to construct automatically-verifiable proofs in propositional and predicate logic. We will discuss topics such as soundness, completeness, relationships to semantic models of truth, and connections among logic, functional programming, and type theory. We will then use the Coq proof assistant to further explore the ideas of machine-checked mathematical theorems and verified software.
The course is aimed at students with good mathematical aptitude and reasonable programming skills, but my intention is to provide suitable challenge, not extreme difficulty. I believe that many of these ideas will work in a regular offering of CS 245, and I hope to test that theory soon. For this offering, I will be providing more not-for-credit exercises and optional extra readings than usual, in the hope that students willing to take an "enriched" course will sometimes do things that do not contribute directly to their final grade.
You will be granted instructor consent if you earned a grade of 85% or higher in CS 145 (or 90% or higher in CS 135) and there is still space in the course. A mark this high in Math 135/145 would be a good idea, but it is not required. Since 245E is not in the university calendar yet, it does not officially exist as far as the university is concerned. For administrative purposes (enrollment, exam schedule, etc.) CS 245E will be considered one section of CS 245. Enrollment will be done "by hand", and you need to email me from your UW email address, including your full name and student ID number. You may also request instructor consent to enroll if you do not meet the criteria above; please include an informal transcript, and reasons why you should be allowed into the course.
Necessary background: I will expect you to be able to program in full Racket, for which CS 136/146 should be adequate preparation (perhaps with a bit of review). We will be using some Racket features (notably pattern matching and hash tables) which are used in CS 145/146 but not CS 135/136; I have placed my lecture summary of pattern matching on the Handouts page (this also serves as an indication of what CS 245E lecture summaries will look like) so that students who did not take CS 145 can catch up. At points, students who took CS 145/146 will have a slight advantage in having seen some ideas before, but I will try to make sure that students who have not seen these ideas are not disadvantaged.
I won’t expect you to remember specific theorems from Math 135, but I will expect you to remember the ideas of proof that were covered there, perhaps upon being reminded by me. For those who took Math 145, you may have been expected to pick up such ideas indirectly from the material, and you may need to work a little to articulate them in your mind.