Readings will come from the following draft textbook chapters. I suggest that if you read online and if you take digital notes, that we all use the included collaborative note-taking software.

  1. Introduction (NB. Every subsequent chapter also includes Ch. 1, so I do not link it here.)
  2. The ACL2 Programming Language
  3. Propositional Logic
  4. Equational Reasoning
  5. Definitions and Termination
  6. Induction
  7. Steering ACL2s
  8. Abstract Data Types and Observational Equivalence
  9. Reasoning About Imperative Code
  10. An ACL2 Reference