3 Handouts
Lecture notes: my prepared commentary on PLFA.
Starter files: locally-adapted versions of the Agda files that make up the textbook. This is the starting point for interactive development.
Completed files: the final product of 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, Alt-click or right-click, depending on your system and browser.
Starter files:
Demo: Agda in action (747demo.agda)
Naturals: Introduction; defining and working with natural numbers. (747Naturals.agda)
Induction: Proving properties of the natural numbers using induction. (747Induction.agda)
Relations: Defining and using relations such as less-than-or-equal-to. (747Relations.agda)
Equality: How propositional equality is defined in Agda. (747Equality.agda)
Isomorphism: Defining and demonstrating isomorphisms. (747Isomorphism.agda)
Connectives: The logical connectives conjunction, disjunction, and implication. (747Connectives.agda)
Negation: How logical negation is defined and used. (747Negation.agda)
Quantifiers: Universal and existential quantification. (747Quantifiers.agda)
Decidable: Decision procedures that produce evidence. (747Decidable.agda)
Lists: Lists in Agda. (747Lists.agda)
Lambda: The simply-typed lambda calculus: syntax, semantics, typing. (747Lambda.agda)
LambdaDefs: Relevant definitions from Lambda, for use below. (747LambdaDefs.agda)
Properties: Theorems about STLC, including progress and preservation. (747Properties.agda)
DeBruijn: Intrinsically-typed de Bruijn representation of STLC. (747DeBruijn.agda)
DBDefs: Relevant definitions from de Bruijn, for use below. (747DBDefs.agda)
More: Adding more constructs to STLC. (747More.agda)
Inference: Computing types from minimally-annotated terms. (747Inference.agda)
Untyped: Changing some of the language design choices made previously. (747Untyped.agda)