Highlights for Review

* PLFA is an online textbook, available at

    plfa.inf.ed.ac.uk

* The proofs for a textbook on programming
  languages can be written in Agda,
  without a separate scripting language.

* Constructive proofs of preservation and
  progress give rise to a prototype evaluator.

* Using raw, extrinsically-typed terms
  is less perspicuous than using
  intrinsically-typed terms.

* An online final examination with access to a
  proof assistant can lead to flawless student
  performance.