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