michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

started to write Modules and Collections

Browse source
This commit is contained in:
wadler 2018-04-17 19:28:17 -03:00
parent ede0c7cc1b
commit c12ce5c3d9
1 changed files with 5 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/Preface.lagda
View file

@ -28,12 +28,11 @@ 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
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
TA][ta].
Benjamin Pierce's excellent [TAPL][tapl], 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 TA][ta].
However, after five years of experience, I have come to the conclusion
that Coq may not be the best vehicle. Too much of the course needs to