csci8980-f21/papers/scp/highlights.txt
2020-03-04 19:16:18 -03:00

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.