Please read lecture notes as soon as they are posted. Send Feedback! If you find errors, we'll give you extra credit. However, the errors have to be in the latest version of the notes. As the class progresses, we will unlock new chapters in the notes. Each time a new chapter is unlocked, we will add an entry in the table below.
Date |
Topic |
Notes |
| 3 Sept 2019 | ACL2s Language Reference | This may be updated as we define more functions |
| 3 Sept 2019 | The ACL2s Programming Language (Chapters 1 and 2) | |
| 19 Sept 2019 | Propositional Logic (Chapter 3) | |
| 01 Oct 2019 | Equational Reasoning (Chapter 4) | |
| 18 Oct 2019 | Definitions and Termination (Chapter 5) | |
| 31 Oct 2019 | Induction (Chapter 6) | |
| 17 Nov 2019 | Steering ACL2s (Chapter 7) | We will not cover this material in class. It is released FYI. |
| 17 Nov 2019 | Abstract Data Types and Observational Equivalence (Chapter 8) | We will only briefly cover this material in class. |
| 17 Nov 2019 | Reasoning about Imperative Code (Chapter 9) | We will only briefly cover this material in class. |