Date	Day	Lecture Topic	Notes Covered (Expected to pre-read)	Assigned HW	Assigned HW Content	Due HW	Friday Lab Content
9/9/20	Wed.	Welcome, why?, website, what’s where, programming review	Website	HW1	Setup, Config
9/10/20	Thurs.	Programming review, datatypes, expressions, primitives’ syntax & semantics	1-2.4 + REPL + ACL2 Ref				Setup, Config
9/14/20	Mon.	The ACL2 environment: ACL2 design: contracts, termination	2.5-2.10	HW2	My first ACL2HW, functions	HW1
9/16/20	Wed.	The dirty dozen: quote let datatype enum range product, etc	2.11-2.13
9/17/20	Thurs.	Property based-testing	2.14-2.17				My first ACL2HW, functions
9/21/20	Mon.	Boolean logic, truth tables, formulae,	3-3.2	HW3	Syntax, Semantics, instantiation	HW2
9/23/20	Wed.	Complexity, P ?= NP, proofs: instantiation, cases, eqnl proofs, decision procs	3.3-3.5
9/24/20	Thurs.	Boolean logic in ACL2s, normal forms, set theory, applications	3.6-3.10				Syntax and Semantics of a lang
9/28/20	Mon.	Limitations of boolean logic, Equational reasoning for programs	4	HW4	Propositional Logic, Truth Tables (+ Project Proposals)	HW3
9/30/20	Wed.	Axioms for equality cons/car/cdr rules,	4.1
9/31/20	Thurs.	Conjectures, ACL2s conjectures,	4.2-4.4				Prop Logic, Minimization
10/5/20	Mon.	Undecidability results, reasoning about arithmetic, program equivalence	4.5	HW5	Substitutions, minimization, normalization	HW4
10/7/20	Wed.	Context vs. theorems	4.6
10/8/20	Thurs.	Proving theorems via equational reasoning.	Live Code REPL				Substitutions, minimization, normalization
10/12/20	Mon.	CANCELLED (Columbus Day)		HW6	Proofs over programs
10/14/20	Wed.	Definition, soundness termination, contracts, acl2 definition principle	5.1			HW5 + Pro. Proposal
10/15/20	Thurs.	Termination, measure functions, project
10/19/20	Mon.	Showing soundness of common recursion schemes via termination; big O analysis wrt terminations	5.2-5.3	HW7		HW6
10/21/20	Wed.	Undecidability of the Halting problem, proof by contradiction,	5.4-5.5 “Snooping”
10/22/20	Thurs.	Mathematical induction, well-foundedness, correctness of math. induction, extracting induction schemes	6-6.2
10/26/20	Mon.	Proving program correctness via induction	6.3	HW8		HW7
10/28/20	Wed.	Data-function-induction trinity; why termination matters	6.4-6.6
10/29/20	Thurs.	Induction like a professional; reasoning about algs, generalization, lemma generation,	6.7
11/2/20	Mon.	Intro to reasoning w/accumulators; tail recursion, efficiency considerations;	6.8	HW9		HW8
11/4/20	Wed.	Project discussion	6.9
11/5/20	Thurs.	Prior proof presentation	6.9				Accumulator try-out + real proving
11/9/20	Mon.	proving correctness wrt accs; Accumulator reasoning	6.9	HW10	A chonky accumulator proof	HW9 + Project
11/11/20	Wed.	CANCELLED (Veteran’s Day) Bonus???
11/12/20	Thurs.	Logic programming and Prolog	“Predicate Logic as …”, Downward				Accumulator Proofs + LP Racket Set-up
11/16/20	Mon.	miniKanren introduction	Presentation/Talk Walk-through	HW11	My first miniKanren programs	HW10
11/18/20	Wed.	microKanren implementation	Paper		(Please plan on meeting w/me on or by here)
11/19/20	Thurs.	microKanren implementation II					miniKanren Basics (Nothing due)
11/23/20	Mon.	Interpreter Lecture				HW11
11/25/20	Wed.	CANCELLED (Thanksgiving Recess)
11/26/20	Thurs.	CANCELLED (Thanksgiving Recess)
11/30/20	Mon.	Inference and judgment	miniKanren Type Inference, Type Inhabitation	HW12	Type inferencer, inhabiter	Project Status Report
12/2/20	Wed.	Type inference II & judgments
12/3/20	Thurs.	miniKanren constraint systems	Slides + (Optional!)				more intepreter + Type inference (nothing due)
12/7/20	Mon.	Relational interpreters	None. Expect surprise			HW12
12/9/20	Wed.	What you could have learned in this class				Project, Presentation