CSCI 54 “Discrete Math and Functional Programming” is the second course in our computer science sequence. Its goals are twofold: to give you a solid foundation for programming and to introduce you to formal proof.
From the course catalog:
A combined course on functional programming and formal proof. Students write programs over a variety of data structures, proving their programs correct with respect to precise logical specifications. Programming topics (and proof topics) range over: recursion (induction); combinatorics; algebraic data types, from lists to trees to abstract syntax trees (structural induction); parsers and interpreters (soundness properties); regular expressions (set theory and language theory).
Prerequisites: CSCI051 PO or equivalent (e.g., 4 or 5 on AP CS exam).
This course is taught by Michael Greenberg. The TAs are Jan Charatan, Ethan Horton, Grace Li, and Millie Mince.
We'll be using Zulip to chat. Contact Prof. Greenberg if you haven't received an invite or are having trouble logging on.
You must have taken some version of CS 051 or an equivalent, like getting a 4 or 5 on the AP CS exam. Since this course is part of the Pomona introductory sequence, you may not take this course if you've already started the Harvey Mudd introductory sequence.
We’ll be using Coq 8.12.0, though any version 8.9.1 or later should work.
We'll be using Emacs and Proof General to edit Coq code. We recommend Emacs or Overleaf for editing LaTeX later in the course.
The course home page has a listing of the planned material. Lectures are posted as pre-recorded videos on Box. Class is lab meets Q&A meets long-form free jazz jam session.
Two thirds of the course will use Coq as the main grader: if Coq accepts your proof, it’s correct! The remaining third of the course will be on paper proofs, which will be graded by hand. There will be in-class quizzes, but they will not be for credit.
Your grade for the course will be determined by your aggregate grades on:
Each homework and midterm will have a variable number of points. Homeworks are all weighted equally to account for 30% of the course; midterms are also weighted equally.
Each class day corresponds to a short homework. Homework is due at 4pm PT on Sunday; submission is on gradescope.
Homework will be a mix of Coq programs, Coq proofs, and paper
proofs. Coq code will be turned in as a .v file; paper proofs will
be turned in as PDFs rendered by LaTeX.
Homework that doesn’t compile, due to syntax or type errors, gets no points.
This course is rife with dependencies and is very homework-oriented; almost all of the learning you do will happen while you’re doing homework! (We think the lectures are good too, but let's not get ahead of ourselves.)
Accordingly, late work will not contribute to your grade. We will, however, review it with you.
Learning any new language is challenging, and Coq is very different from conventional programming languages. We encourage you to help each other learn the language and we also encourage you to discuss the text.
However: all work in the course must be your own. As explained in the student handbook, this means that the work you turn in must represent only your own work. It must not be based on help from others or information obtained from sources other than those approved by the instructor. Examples of acceptable sources of information include:
Examples of unacceptable sources of information include Stack Overflow, Quora, and your classmates’ code.
You should never read or copy another student’s solutions (code or otherwise), exchange files, or share your solutions with anyone else in the class until after everyone involved has turned in their work. If a discussion with another student helped you find your answer, mention that in a comment. It’s hard to tell the difference between uncredited help and plagiarism (because they’re the same thing).
If any of this is unclear, please: just ask.
Failure to abide by these rules is considered plagiarism, and will result in severe penalties. The first offense typically results in failing the assignment and referral to the appropriate college office or committee—which may mean further consequences. See the CS Academic Honesty Policy and Pomona Academic Standards for further information. Please don’t put anyone—me, you, or anyone else—in this unpleasant situation.
Pomona students seeking academic accommodations should contact disability support at the Dean of Students Office. You’ll need to meet with them to discuss appropriate accommodations and provide documentation as necessary.
Students from other colleges should contact their home college’s disability coordinator for accommodations. The coordinators are, to the best of our knowledge:
This is the fourth run of this course, but with heavy, heavy revisions. It's a crazy, awful time. Let’s make a deal. Our side: if things aren’t working, we’ll change them. Your side: if things aren’t working, you’ll tell us.