From ede0c7cc1bec84e29e86bf347aedf31809b0d7ba Mon Sep 17 00:00:00 2001 From: wadler Date: Tue, 17 Apr 2018 17:38:51 -0300 Subject: [PATCH] more fixes to Preface --- src/Lists.lagda | 1 + src/Preface.lagda | 3 ++- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Lists.lagda b/src/Lists.lagda index 4f543f85..1a5dfd1d 100644 --- a/src/Lists.lagda +++ b/src/Lists.lagda @@ -872,6 +872,7 @@ Do we also have the following? If so, prove; if not, explain why. + ## Standard Library Definitions similar to those in this chapter can be found in the standard library. diff --git a/src/Preface.lagda b/src/Preface.lagda index 8cf1b6b0..c29809d7 100644 --- a/src/Preface.lagda +++ b/src/Preface.lagda @@ -28,7 +28,8 @@ an excellent time to comment on the first part. Since 2013, I have taught a course on Types and Semantics for Programming Languages to fourth-year undergraduates and masters students at the University of Edinburgh. That course is not based on -TAPL, but on Pierce's subsequent textbook, [Software Foundations][sf], +the excellent [Types and Programming Languages][tapl] by Benjamin +Pierce, but on Pierce's subsequent textbook, [Software Foundations][sf], written in collaboration with others and based on Coq. I am convinced of Pierce's claim that basing a course around a proof assistant aids learning, as summarised in his ICFP Keynote, [Lambda, The Ultimate