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

more fixes to Preface

Browse source
This commit is contained in:
wadler 2018-04-17 17:38:51 -03:00
parent 715cfb7fcc
commit ede0c7cc1b
2 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lists.lagda
View file

@ -872,6 +872,7 @@ Do we also have the following?
If so, prove; if not, explain why. If so, prove; if not, explain why.
## Standard Library ## Standard Library
Definitions similar to those in this chapter can be found in the standard library. Definitions similar to those in this chapter can be found in the standard library.

3
src/Preface.lagda
View file

@ -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 Since 2013, I have taught a course on Types and Semantics for
Programming Languages to fourth-year undergraduates and masters Programming Languages to fourth-year undergraduates and masters
students at the University of Edinburgh. That course is not based on 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 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 of Pierce's claim that basing a course around a proof assistant aids
learning, as summarised in his ICFP Keynote, [Lambda, The Ultimate learning, as summarised in his ICFP Keynote, [Lambda, The Ultimate