added comment and citations about type systems

book.bib

@@ -1,4 +1,32 @@
 
+@book{Pierce:2004fk,
+	editor = {Benjamin C. Pierce},
+	publisher = {The MIT press},
+	title = {Advanced Topics in Types and Programming Languages},
+	year = {2004}}
+
+@book{Pierce:SF2,
+  author = {Benjamin C. Pierce and Arthur Azevedo de Amorim
+                  and Chris Casinghino and Marco Gaboardi and
+                  Michael Greenberg and C\v{a}t\v{a}lin Hri\c{t}cu
+                  and Vilhelm Sj\"{o}berg and Andrew Tolmach
+                  and Brent Yorgey},
+  title = {Programming Language Foundations},
+  series = {Software Foundations series, volume 2},
+  month = may,
+  year = {2018},
+  publisher = {Electronic textbook},
+  plclub = {Yes},
+  bcp = {Yes},
+  keys = {verification,books}
+}
+
+@Book{Harper2016,
+  author = 	 {Robert Harper},
+  title = 	 {Practical Foundations for Programming Languages},
+  publisher = 	 {Cambridge University Press},
+  year = 	 2016,
+  edition = 	 {2nd}}
 
 @Article{Appel90,
   author = 	 {Appel, Andrew W.},

book.tex

@@ -6533,12 +6533,15 @@ of \racket{\code{(car 1)}}\python{\code{1[0]}}, \racket{Typed
 \python{stating that a ``value of type \code{int} is not indexable''.}
 
 The \LangIf{} language performs type checking during compilation like
-\racket{Typed Racket}\python{MyPy}. In Chapter~\ref{ch:Ldyn} we study the
-alternative choice, that is, a dynamically typed language like
-\racket{Racket}\python{Python}.
-The \LangIf{} language is a subset of \racket{Typed Racket}\python{MyPy};
-for some operations we are more restrictive, for example, rejecting
-\racket{\code{(not 1)}}\python{\code{not 1}}.
+\racket{Typed Racket}\python{MyPy}. In Chapter~\ref{ch:Ldyn} we study
+the alternative choice, that is, a dynamically typed language like
+\racket{Racket}\python{Python}.  The \LangIf{} language is a subset of
+\racket{Typed Racket}\python{MyPy}; for some operations we are more
+restrictive, for example, rejecting \racket{\code{(not
+    1)}}\python{\code{not 1}}. We keep the type checker for \LangIf{}
+fairly simple because the focus of this book is on compilation, not
+type systems, about which there are already several excellent
+books~\citep{Pierce:2002hj,Pierce:2004fk,Harper2016,Pierce:SF2}.
 
 This chapter is organized as follows.  We begin by defining the syntax
 and interpreter for the \LangIf{} language