20 lines
512 B
Text
20 lines
512 B
Text
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.
|