3 Handouts

The materials linked below include:
  • Lecture notes: textual summaries of my in-lecture commentary on PLFA. These will be updated after each lecture. They are not a substitute for attending!

  • Starter files: locally-adapted versions of the Agda files that make up the textbook. This is where we will start in-class interactive development.

  • Completed files: the final product of in-class interactive development. Everything is filled in except solutions to exercises. These files form the starting point for assignments.

Warning: The starter and completed files contain Unicode, which your browser is probably capable of displaying, but may not be configured to do so. Do not cut and paste from your browser. Instead, download the files using Command-click, Control-click, or right-click, depending on your system.

Lecture notes on PLFA (by PR)

Starter files:

Completed files: