<!– HAMPATH is NP Complete –> <!– More NP Complete problems –>
<!– | Month | Date | Day | Suggested Spots | Topic | –> <!– | Sept. | 10 | Fri | Topic 1 Why and Theory of Comp | Intro to Theory of Computation | –> <!– | Sept. | 14 | Tues | | Deterministic Finite Automata | –> <!– | Sept. | 17 | Fri | Topic 2 Regular languages | Regular Languages | –> <!– | Sept. | 21 | Tues | | Combining Regular Languages | –> <!– | Sept. | 24 | Fri | Topic 3 Regular languages 2 | Nondeterminism and NFAs | –> <!– | Sept. | 28 | Tues | | NFA → DFA, Reg Exprs | –> <!– | Oct. | 1 | Fri | | More Reg Exprs, Inductive Proofs | –> <!– | Oct. | 5 | Tues | | More Inductive Proofs, Non-reg Langs | –> <!– | Oct. | 8 | Fri | Topic 4 CFG | Pumping Lemma Proof Examples | –> <!– | Oct. | 12 | Tues | Topic 5 CFG DFPDA | Context-free Grammars | –> <!– | Oct. | 15 | Fri | | Pushdown Automata (PDA) CFG ↔ PDA | –> <!– | Oct. | 19 | Tues | Topic 6 Church-Turing thesis | DCFLS, DPDAs, and Parsing | –> <!– | Oct. | 22 | Fri | | Non-CFLs; Intro to TMs | –> <!– | Oct. | 26 | Tues | | Turing Machine Variants | –> <!– | Oct. | 29 | Fri | Topic 7 More on thms, decidability | Decidability and Regular Languages | –> <!– | Nov. | 2 | Tues | | Decidability and CFLs | –> <!– | Nov. | 5 | Fri | | Diagonalization and Undecidability | –> <!– | Nov. | 9 | Tues | Topic 8 Reductions | Reducibility and the Halting Problem | –> <!– | Nov. | 12 | Fri | | Mapping Reducibility | –> <!– | Nov. | 16 | Tues | | Turing Machines and Recursion | –> <!– | Nov. | 19 | Fri | Topic 9 Time complexity | Intro to Time Complexity | –> <!– | Nov. | 23 | Tues | | Polynomial Time (P) | –> <!– | Nov. | 26 | Fri | | Thanksgiving Break | –> <!– | Nov. | 30 | Tues | Topic 10 NP Completeness | NP | –> <!– | Dec. | 3 | Fri | | Poly-time Reducibility, NP Completeness | –> <!– | Dec. | 7 | Tues | | Cook-Levin theorem | –> <!– | Dec. | 10 | Fri | Topic 11 dealing w/NP completeness | Recap & Dealing with NP Completeness | –>
| Date | Day | Lab/Lecture Topic | Assigned HW | Notes Covered (Expected to pre-read) |
| 1/20/21 | Wednesday | Welcome; why?; website; what’s where; programming review | HW1 - Setup; Config | Ch1-2.4 + Website |
| 1/21/21 | Thursday | Programming review; datatypes; expressions; primitives’ syntax & semantics | 1-2.4 + REPL + ACL2 Ref | |
| 1/22/21 | Friday | Setup; Config | ||
| 1/25/21 | Monday | The ACL2 environment: ACL2 design: contracts; termination | HW2 - My first ACL2HW; functions | 2.5-2.10 |
| 1/27/21 | Wednesday | The dirty dozen: quote let datatype enum range product; etc | 2.11-2.13 | |
| 1/28/21 | Thursday | Property based-testing | 2.14-2.17 | |
| 1/29/21 | Friday | My first ACL2HW; functions | ||
| 2/1/21 | Monday | Boolean logic; truth tables; formulae; | HW3 - Propositional Logic; Truth Tables | 3-3.2 |
| 2/3/21 | Wednesday | substitution, instantiation, reasoning, proofs, matching. | 3.3-3.4 | |
| 2/4/21 | Thursday | Boolean logic in ACL2s; normal forms; applications; Complexity; P ?= NP; decision procs | 3.5-3.7 | |
| 2/5/21 | Friday | Prop Logic; Minimization | ||
| 2/8/21 | Monday | Limitations of boolean logic; relationships w/set theory | HW4 - Syntax; Semantics; instantiation | 3.8, 4 |
| 2/10/21 | Wednesday | Conjectures; ACL2s conjectures; | 4.1 | |
| 2/11/21 | Thursday | Program equivalence; Additional axioms (cons/car/cdr rules); Context vs. theorems | 4.2-4.3 | |
| 2/12/21 | Friday | Syntax and Semantics of a lang | ||
| 2/15/21 | Monday | NO CLASS - HOLIDAY | HW5 - Substitution; normalization; equational reasoning | |
| 2/17/21 | Wednesday | Proving theorems via equational reasoning; reasoning about arithmetic | 4.5-6 | |
| 2/18/21 | Thursday | Recapitulate proving theorems via equational reasoning. | [M1]({{ site.baseurl }}/assets/code/len-cons-add.txt) [A1]({{ site.baseurl }}/assets/code/cons-app-proof.txt) [M2]({{ site.baseurl }}/assets/code/rev-singleton.txt) [A2]({{ site.baseurl }}/assets/code/in-singleton.txt) [M3]({{ site.baseurl }}/assets/code/xfq.txt) | |
| 2/19/21 | Friday | Substitutions; minimization; normalization | ||
| 2/22/21 | Monday | Definition; soundness termination; contracts; acl2 definition principle | HW6 - Practice Exam; Admissability | 5.1 |
| 2/24/21 | Wednesday | Termination; measure functions; | 5.1 | |
| 2/25/21 | Thursday | Showing soundness of common recursion schemes via termination | 5.2 | |
| 2/26/21 | Friday | Midterm exam review | ||
| 3/1/21 | Monday | Undecidability; the Halting problem; proofs by contradiction | HW7 - Measures; Undecidability and induction | 5.4-5.5 |
| 3/3/21 | Wednesday | More undecidability; consequences; | 4.4, 5.4-5.5 [“Scooping”](http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html) | |
| 3/4/21 | Thursday | Mathematical induction; well-foundedness; correctness of math. induction; extracting induction schemes | 6-6.2 | |
| 3/5/21 | Friday | |||
| 3/8/21 | Monday | Proving program correctness via induction | HW8 - More induction | 6.3 |
| 3/10/21 | Wednesday | Data-function-induction trinity; why termination matters | 6.4-6.6 [app2-assoc-1]({{ site.baseurl }}/assets/code/app-app-morning.txt) [app2-assoc-2]({{ site.baseurl }}/assets/code/app2-assoc-aft.txt) | |
| 3/11/21 | Thursday | Induction like a professional; reasoning about algs; generalization; lemma generation; | 6.7 | |
| 3/12/21 | Friday | |||
| 3/15/21 | Monday | Intro to reasoning w/accumulators; tail recursion; efficiency considerations; | HW9 - Larger Proofs | 6.8 |
| 3/17/21 | Wednesday | proving correctness wrt accs; Accumulator reasoning | 6.9 [revt-equal]({{ site.baseurl }}/assets/code/revt-equal.txt) | |
| 3/18/21 | Thursday | Abstract Data Types | 8.1-8.3 | |
| 3/19/21 | Friday | Accumulator try-out + real proving | 7 | |
| 3/22/21 | Monday | SAT/SMT/CP | HW10 - Accumulator proofs *Due 1wk later than usual | |
| 3/24/21 | Wednesday | NO CLASS - HOLIDAY | ||
| 3/25/21 | Thursday | SAT/SMT/CP | [test.cnf]({{ site.baseurl }}/assets/code/test.cnf) [try2.cnf]({{ site.baseurl }}/assets/code/try2.cnf) | |
| 3/26/21 | Friday | Using real ACL2 | 7 | |
| 3/29/21 | Monday | Logic programming and Prolog | [Predicate Logic as …]({{ site.baseurl }}/assets/docs/Kowalski74.pdf) [Downward]({{ site.baseurl }}/assets/docs/Downward_Chs_1-5.pdf) | |
| 3/31/21 | Wednesday | miniKanren introduction | [mk1.rkt]({{ site.baseurl }}/assets/code/mk1.rkt) [Presentation/Talk](https://www.youtube.com/watch?v=RG9fBbQrVOM) | |
| 4/1/21 | Thursday | microKanren implementation | [micro-day-1.rkt]({{ site.baseurl }}/assets/code/micro-day-1.rkt) | |
| 4/2/21 | Friday | Accumulator Proofs + LP Racket Set-up | ||
| 4/5/21 | Monday | Project description talk-through | HW11 - My first miniKanren programs | |
| 4/7/21 | Wednesday | microKanren implementation II | [micro-2.rkt]({{ site.baseurl }}/assets/code/micro-2.rkt) [Paper](https://dl.acm.org/citation.cfm?doid=2989225.2989230) | |
| 4/8/21 | Thursday | Interpreter Lecture | [lang.rkt]({{ site.baseurl }}/assets/code/lang.rkt) | |
| 4/9/21 | Friday | miniKanren Basics (Nothing due) | ||
| 4/12/21 | Monday | NO CLASS - HOLIDAY | HW12 - Types and Type Inference | |
| 4/14/21 | Wednesday | more Intepreter + Type inference | ||
| 4/15/21 | Thursday | Type inference II & judgments | ||
| 4/16/21 | Friday | Types Behavior | ||
| 4/19/21 | Monday | Surprise | None. Expect surprise | |
| 4/21/21 | Wednesday | What you could have learned in this class |