There is no required or recommended textbook. I have included a number of references in the lecture summaries and on the Resources page, but not with the intention that they directly support course material. Differences in notation, meaning, definitions, assumptions, and order of coverage are likely to render most potential references more confusing than illuminating. If you are having difficulty with course material, please contact course personnel rather than try to find something online or in the library that might help. I’m sorry to not be able to recommend any backup materials, but this is what happens when a course is a synthesis of various sources. I’m open to creating supplementary documents as needed. What I will not do is provide more examples, because I want to encourage engagement with the underlying theory. At this point in your education, and particularly in an enriched course, you should not be trying to learn based on a large corpus of examples.
We will be using Piazza for online public questions and discussion. If you have not gotten an invitation by the first lecture, or you join the course late, please contact the instructor. Course personnel will have regular office hours, listed on the home page. You may also email course personnel. Please do so from your UW email address.
These will be in the style of my CS 145/146 offerings (2008-2014), with sparse slides that will not be posted, supplemented with occasional boardwork. After each lecture I will post detailed lecture summaries on the Handouts page, again in the style of CS 145/146 (my summaries were used in those courses in 2015-2016, even though I did not teach those offerings; they were not used in the fall 2016 offering of CS 145). I suggest taking selective notes by hand in lecture, more as a stimulus for active learning than for reference later. Consider avoiding open laptops and tablets in lecture. They are distracting to you and others, and studies show they reduce performance even when used only to take notes (which is rarely their only use in practice). Please set your cellphones on stun.
Do not make the mistake of thinking that the lecture summaries are a substitute for attending lecture. I will not in any way enforce regular lecture attendance, but I highly recommend it. I will do my best to make it worth your while.
I may use some tutorial hours as additional lecture hours to make up for absences due to travel. I will lecture in some of the tutorial hours, sometimes on required material, sometimes on optional material. Other tutorial hours may be used by the IA and/or TAs for various purposes. We will inform you on a weekly basis.
Details will be posted on the Assignments page. Assignment questions will not be due weekly or on a regular schedule; rather, each assignment will be released when relevant material has been covered in lecture. I will try to give some advance warning, but it really depends on the timing of lectures, and all I can do is post estimates. Submission details are on the Marmoset page.
Assignment questions will primarily involve programming parts of several versions of a proof assistant in Racket, and using those programs to develop and check proofs of theorems. I may also assign some "written" (typed or typeset) proofs of metamathematical theorems as well. Different questions may have different weights. No solutions will be posted, but course personnel will be happy to help you complete questions for study purposes.
One midterm exam and one final exam, at the same times as the CS 245 (regular section) exams. Midterm timing is available in Quest; room details will be posted here. Final exam details will be posted here, but you can learn about it from the Registrar’s web page at the same time as we do. Our exams will be completely different from those for the regular sections.
There will be no practice exams or exam questions available. It is a bad idea in general to try to study from previous exams. Your best approach is to complete all assignment questions, even if the due date has passed, and work on your own variations of these questions as well. Note that the assignments make heavy use of computers but the exams do not; they are entirely handwritten. My exam questions are not tweaks on assignment questions. I try to find new situations that you should be able to handle if you have done the assignments and learned the concepts that need to be applied.
Assignments will be worth 20%; midterm 35%; final exam 45%.
We will be using Racket 6.8. We will see Agda in tutorial but you will not be required to install it or to use it.
We will also be using Coq 8.6. You will need to download and install this on a machine of your choice (the Coq compiler is available on the CS General and CS Undergraduate Environments, but not the IDEs described next).
You can either use the CoqIDE application (available from the page above) to work in Coq, or (as will be done in lecture) Proof General for Emacs. Either choice is adequate for completing course work, but CoqIDE is much simpler to install. There is more overhead both in installing Emacs and in learning to use it, but you can use it for many other purposes, and if you already know it, this is a better choice. Power users may wish to investigate the Company-Coq extensions to Proof General.