Homework is generally due at 11pm PT on Sundays.
|12-14||Final exam slot, retakes|
Feel free to look at various chapters ahead of time, but know that we may change assignments up until a week before the due date!
Worksheets are not for credit; they are excellent practice, though, and they resemble the kinds of problems we like to set on exams.
Guides are meant to give you an overview of proof techniques or how to prepare for an upcoming test.
Office hours and mentor sessions are in the same Zoom room. The password is available on Slack.
All times are in Pacific Time. Look in
#csci-054-po on Slack for Zoom info. Look for more times to be announced after Tuesday 09/07.
|Summer 07:30pm--09:30pm||Prof Osborn 02:00pm--04:00pm||Prof Osborn 09:00--11:00||Guy 09:00--11:00|
|LC 1 (Summer) 09:00--11:00||LC 4 (Guy) 05:30pm--07:30pm||Chloe 11:00--1:00||Lucas & David 06:00pm--08:00pm|
|LC 2 (Eryn) 11:00-01:00pm||Eryn 05:00pm--07:00pm||LC 5 (Lucas) 03:00pm--05:00pm|
|LC 3 (Chloe) 01:00pm--02:00pm||LC 6 (David) 03:00pm--05:00pm|
Please see the syllabus for general course information. The course has three parts: programming, formal proof, and paper proof.
|01||08-31||Day01_intro||Coq, Emacs, how to read the book; boolean operations, truth tables, and DNA bases|
|02||09-02||Day02_types||numbers and recursive functions|
|03||09-07||Day03_recursion||more recursive functions|
|04||09-09||Day04_structures||pairs, options, lists, and trees|
|07||09-21||Day07_trees||binary search trees|
|08||09-23||Day08_sets||list and tree representations of sets|
|09||09-28||Day09_levenshtein||the Levenshtein algorithm for edit distance|
|10||09-30||Day10_expressions||expressions and interpreters|
At this point, we'll have our first exam on gradescope, about programming.
|11||10-05||Day11_propositions||basic formal proof; Coq tactics; equality and logical propositions|
|12||10-07||Day12_cases||proofs by case analysis|
|15||10-21||Day15_induction2||induction on other structures|
|17||10-28||Day17_indprop2||inductive propositions, continued|
|18||11-02||Day18_sorting||permutations and sorting|
|19||11-04||Day19_levenshtein||proving the Levenshtein algorithm correct and optimal|
At this point, we'll have our second exam on gradescope, about formal proof.
|20||11-09||Day20_latex||mathematical typesetting in LaTeX|
|21||11-11||Day21_translating||translating formal proofs to paper|
|23||11-18||Day23_combinatorics||counting; sum rule, product rule, division rule, permutation, choose|
|25||11-30||Day25_relations||relations and functions|
|26||12-02||Day26_countability||cardinality and (un)countability|
|27||12-07||Day27_graphs||graphs and paths and trees|
The third exam (on informal proof) is due the Sunday after the last week of classes (12/12). Grades will be distributed by the morning of 12/14.
Retakes of exam sections will take place during our final exam slot (14:00--17:00 PT, Tuesday December 14th), in-person but laptops allowed.
To configure your emacs, you'll want to download our init.el and install it to the appropriate location:
init.elin a folder in your home directory called
.emacs.d(the leading dot is important!), and be sure you have no file called
.emacsin your home directory. This is easiest in the terminal (
rm ~/.emacs ; mkdir -p ~/.emacs.d ; mv ~/Downloads/init.el ~/.emacs.d).
init.elin a folder called
.emacs.d(the leading dot is important!) in