### 3` `Handouts

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.

Starter files:

Naturals: (Sep. 4, 10) Introduction; defining and working with natural numbers. (842Naturals.agda)

Induction (Sep. 10, 12): Proving properties of the natural numbers using induction. (842Induction.agda)

Relations (Sep. 12, 17, 19): Defining and using relations such as less-than-or-equal-to. (842Relations.agda)

Equality (Sep. 19): How propositional equality is defined in Agda. (842Equality.agda)

Isomorphism (Sep. 24): Defining and demonstrating isomorphisms. (842Isomorphism.agda)

Connectives (Sep. 26, Oct. 1): The logical connectives conjunction, disjunction, and implication. (842Connectives.agda)

Negation (Oct. 1, 3): How logical negation is defined and used. (842Negation.agda)

Quantifiers (Oct. 3, 8): Universal and existential quantification. (842Quantifiers.agda)

Decidable (Oct. 8, 10): Decision procedures that produce evidence. (842Decidable.agda)

Lists (Oct. 22, 24): Lists in Agda. (842Lists.agda)

Lambda (Oct. 24): The simply-typed lambda calculus: syntax, semantics, typing. (842Lambda.agda)

Properties: Theorems about STLC, including progress and preservation. (842Properties.agda)

DeBruijn: Intrinsically-typed de Bruijn representation of STLC. (842DeBruijn.agda)

More: Adding more constructs to STLC. (842More.agda)

Inference: Computing types from minimally-annotated terms. (842Inference.agda)

Untyped: Changing some of the language design choices made previously. (842Untyped.agda)