Notes on PLFA

\(\newcommand{\la}{\lambda} \newcommand{\Ga}{\Gamma} \newcommand{\ra}{\rightarrow} \newcommand{\Ra}{\Rightarrow} \newcommand{\La}{\Leftarrow} \newcommand{\tl}{\triangleleft} \newcommand{\ir}[3]{\displaystyle\frac{#2}{#3}~{\textstyle #1}}\)

(Prabhakar Ragde, 2021)

These notes provide additional commentary (or gloss, or a remix) on/of the textbook "Programming Language Foundations in Agda" by Wadler, Kokke, and Siek, in the context of CS 747 at the University of Waterloo in Winter 2022.

Thanks to Wen Kokke and David Darais for helpful discussions and answers to my questions, and to the students of CS 842 who provided useful feedback, particularly Miti Mazumdar.