diff --git a/courses/tspl/2019/tspl2019.md b/courses/tspl/2019/tspl2019.md index e556a351..8a1a096d 100644 --- a/courses/tspl/2019/tspl2019.md +++ b/courses/tspl/2019/tspl2019.md @@ -152,13 +152,31 @@ but talk to me if you want to formalise something else. examination with the Agda proof assistant, under DICE to let you practice for the exam and familiarise yourself with exam conditions. + +## Additional reading + +* John Reynolds, + [Three Approaches to Type Structure][reynolds], + _Mathematical Foundations of Software Development_, + LNCS 185, pages 97–138, 1985. + +* Barendregt, H. P. + [Introduction to generalized type systems][barendregt] + _Journal of Functional Programming_, 1(2): 125–154, 1991. + +[reynolds]: http://homepages.inf.ed.ac.uk/wadler/papers/reynolds/three-approaches.pdf + +[barendregt]: http://homepages.inf.ed.ac.uk/wadler/papers/barendregt/pure-type-systems.pdf + + +