1 For Prospective Students
In this course, we will will work through the online textbook Programming Language Foundations in Agda (PLFA) by Wen Kokke and Philip Wadler, available in full online. The goal of this book, and our goal, is to study topics in functional programming, logic, semantics, and type theory using the Agda programming language. This is the same goal as my version of CS 798 (Software Foundations) that I have taught three times, most recently in Fall 2018, using the Coq programming language. The reasons I am switching to Agda are largely articulated in the preface to PLFA and my own notes on it, found in the Handouts section.
Nonetheless, the preface of the CS 798 textbook, Software Foundations (SF), gives an excellent overview of the topics covered and the reasons to study them; if you are reading this sentence, you should click through and read that preface as well. In addition to what is written in the two prefaces, I can add that working in Agda (or Coq) is an interesting change from conventional (even functional) programming, and will appeal to those who like solving puzzles or playing games.
This course is numbered 842 instead of 798 because of several reasons. PLFA is much newer than SF, and should be considered a work in progress; I have much less experience with teaching using Agda; installation of Agda and the Emacs editor for interactive development is more fraught than installing Coq; and Emacs takes some getting used to if you have not used it before. So there will be a few more rough edges and bumps in this course.
Lectures: The HTML version of PLFA is generated from a set of source files that are written in literate Agda, which intersperses code and commentary. Those source files are available online as well (there is a link at the top of each PLFA chapter). PLFA is hosted on GitHub, so you can download or fork it. We are working from the stable version, but there is a development version with much activity.
I have prepared starter files by stripping out the commentary and most of the completed code, leaving just type definitions and holes to be filled. I have also made a few changes of my own. Those starter files will be available on the Handouts page. Lectures will consist of my loading a starter file into Emacs, and developing the code interactively, while providing relevant commentary and some whiteboard explanations. I will post completed versions that should nearly match what we develop in lecture. (These are essentially my practice for livecoding in class.) We will sometimes look at the PLFA webpages in lecture, in a browser, but mostly I will leave it as reading, with my own notes provided to capture some of my in-lecture elaborations and my reasons for minor changes.
How far we will get depends on many factors. PLFA, like SF, is divided into two volumes, Logical Foundations and Programming Language Foundations. Typically in CS 798, I was able to complete the first volume but had to rush through a third to a half of the second volume. Another reason to use Agda is that there is less first-volume overhead, so the hope is to be able to go further into the second volume than seems possible with SF. PLFA is not a literal translation of SF; it omits some topics and introduces others. So it’s hard to predict what will happen. Based on my working through it, I believe we will get further, but I also have not taught a whole course using Agda before.
We will use Piazza for out-of-class questions and general discussions. If you’re enrolled in the class on the first day, you will receive an invitation; otherwise please contact me and I will add you. Private email to me for questions is also fine, but please send from your UW account if possible, so I can look at any Marmoset submission, in case that helps.
Workload: The starter and completed files include exercises. Once we have finished working on a given file in lecture, I will give you a due date for the corresponding assignment. Some exercises are marked "PLFA exercises"; these appear in PLFA but will not be assigned in this course. You can choose whether or not to work on them. Others are marked "842 exercises", and these are the ones that you will be assigned. Most of these exercises appear in PLFA. Some are new and some have been changed.
The exercises involve writing Agda code interactively, starting with the completed file for a chapter. The code is for the most part short, but it may take you some time to get it right. The advantage of using Agda is that you will know immediately whether the code is correct or not. I have personally completed all exercises I will ask you to do, without the benefit of solutions (none will be posted), and I will have some additional comments and hints to offer. These assignments will be the only basis for your final grade. There are no exams, presentations, or projects.
Relative to other graduate courses at this level, I would characterize the workload as moderate.
Necessary background: I will expect only some familiarity with some form of programming (such as might be obtained from a first course), exposure to university-level mathematics (including the brief look at discrete mathematics and logic that is found in the typical undergraduate CS curriculum), and the ability to install and work with new software (on which the Logistics page has more details). Exposure to functional programming will help, but if you have none, just be prepared to think about programs differently.