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 A1 M2 A2 M3
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”
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 app2-assoc-2
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
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 try2.cnf
3/26/21 Friday Using real ACL2   7
3/29/21 Monday Logic programming and Prolog   Predicate Logic as … Downward
3/31/21 Wednesday miniKanren introduction   mk1.rkt Presentation/Talk
4/1/21 Thursday microKanren implementation   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 Paper
4/8/21 Thursday Interpreter Lecture   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