--- a/latex/cpdt.bib	Sun Apr 22 15:51:03 2012 -0400
+++ b/latex/cpdt.bib	Sun Apr 22 16:25:22 2012 -0400
@@ -414,3 +414,34 @@
  publisher = {ACM},
  address = {New York, NY, USA},
 }
+
+@ARTICLE{whyfp,
+    author = {John Hughes},
+    title = {Why Functional Programming Matters},
+    journal = {The Computer Journal},
+    year = {1984},
+    volume = {32},
+    pages = {98--107}
+}
+
+@Book{Prolog,
+  author       = "Leon Sterling and Ehud Shapiro",
+  title        = "The Art of Prolog, 2nd Edition",
+  year         = "1994",
+  publisher    = "MIT Press"
+}
+
+@Book{LogicProgramming,
+  author       = "John W. Lloyd",
+  title        = "Foundations of Logic Programming, 2nd Edition",
+  year         = "1987",
+  publisher    = "Springer"
+}
+
+@InBook{deriving,
+  title =	 "Haskell 98 Language and Libraries: The Revised Report",
+  author =	 "Simon {Peyton Jones} and Lennart Augustsson and Dave Barton and Brian Boutel and Warren Burton and Joseph Fasel and Kevin Hammond and Ralf Hinze and Paul Hudak and John Hughes and Thomas Johnsson and Mark Jones and John Launchbury and Erik Meijer and John Peterson and Alastair Reid and Colin Runciman and Philip Wadler",
+  year =	 "1998",
+  chapter =      "4.3.3",
+  url =          {http://www.haskell.org/onlinereport/decls.html#derived-decls}
+}

--- a/src/Coinductive.v	Sun Apr 22 15:51:03 2012 -0400
+++ b/src/Coinductive.v	Sun Apr 22 16:25:22 2012 -0400
@@ -18,7 +18,7 @@
 
 (** %\chapter{Infinite Data and Proofs}% *)
 
-(** In lazy functional programming languages like %\index{Haskell}%Haskell, infinite data structures are everywhere.  Infinite lists and more exotic datatypes provide convenient abstractions for communication between parts of a program.  Achieving similar convenience without infinite lazy structures would, in many cases, require acrobatic inversions of control flow.
+(** In lazy functional programming languages like %\index{Haskell}%Haskell, infinite data structures are everywhere%~\cite{whyfp}%.  Infinite lists and more exotic datatypes provide convenient abstractions for communication between parts of a program.  Achieving similar convenience without infinite lazy structures would, in many cases, require acrobatic inversions of control flow.
 
 %\index{laziness}%Laziness is easy to implement in Haskell, where all the definitions in a program may be thought of as mutually recursive.  In such an unconstrained setting, it is easy to implement an infinite loop when you really meant to build an infinite list, where any finite prefix of the list should be forceable in finite time.  Haskell programmers learn how to avoid such slip-ups.  In Coq, such a laissez-faire policy is not good enough.
 

--- a/src/Generic.v	Sun Apr 22 15:51:03 2012 -0400
+++ b/src/Generic.v	Sun Apr 22 16:25:22 2012 -0400
@@ -18,7 +18,7 @@
 
 (** %\chapter{Generic Programming}% *)
 
-(** %\index{generic programming}\textit{%#<i>#Generic programming#</i>#%}% makes it possible to write functions that operate over different types of data.  %\index{parametric polymorphism}%Parametric polymorphism in ML and Haskell is one of the simplest examples.  ML-style %\index{module systems}%module systems%~\cite{modules}% and Haskell %\index{type classes}%type classes%~\cite{typeclasses}% are more flexible cases.  These language features are often not as powerful as we would like.  For instance, while Haskell includes a type class classifying those types whose values can be pretty-printed, per-type pretty-printing is usually either implemented manually or implemented via a %\index{deriving clauses}%[deriving] clause, which triggers ad-hoc code generation.  Some clever encoding tricks have been used to achieve better within Haskell and other languages, but we can do %\index{datatype-generic programming}\emph{%#<i>#datatype-generic programming#</i>#%}% much more cleanly with dependent types.  Thanks to the expressive power of CIC, we need no special language support.
+(** %\index{generic programming}\textit{%#<i>#Generic programming#</i>#%}% makes it possible to write functions that operate over different types of data.  %\index{parametric polymorphism}%Parametric polymorphism in ML and Haskell is one of the simplest examples.  ML-style %\index{module systems}%module systems%~\cite{modules}% and Haskell %\index{type classes}%type classes%~\cite{typeclasses}% are more flexible cases.  These language features are often not as powerful as we would like.  For instance, while Haskell includes a type class classifying those types whose values can be pretty-printed, per-type pretty-printing is usually either implemented manually or implemented via a %\index{deriving clauses}%[deriving] clause%~\cite{deriving}%, which triggers ad-hoc code generation.  Some clever encoding tricks have been used to achieve better within Haskell and other languages, but we can do %\index{datatype-generic programming}\emph{%#<i>#datatype-generic programming#</i>#%}% much more cleanly with dependent types.  Thanks to the expressive power of CIC, we need no special language support.
 
    Generic programming can often be very useful in Coq developments, so we devote this chapter to studying it.  In a proof assistant, there is the new possibility of generic proofs about generic programs, which we also devote some space to. *)
 

--- a/src/LogicProg.v	Sun Apr 22 15:51:03 2012 -0400
+++ b/src/LogicProg.v	Sun Apr 22 16:25:22 2012 -0400
@@ -23,7 +23,7 @@
 
 (** The Curry-Howard correspondence tells us that proving is %``%#"#just#"#%''% programming, but the pragmatics of the two activities are very different.  Generally we care about properties of a program besides its type, but the same is not true about proofs.  Any proof of a theorem will do just as well.  As a result, automated proof search is conceptually simpler than automated programming.
 
-   The paradigm of %\index{logic programming}%logic programming, as embodied in languages like %\index{Prolog}%Prolog, is a good match for proof search in higher-order logic.  This chapter introduces the details, attempting to avoid any dependence on past logic programming experience. *)
+   The paradigm of %\index{logic programming}%logic programming%~\cite{LogicProgramming}%, as embodied in languages like %\index{Prolog}%Prolog%~\cite{Prolog}%, is a good match for proof search in higher-order logic.  This chapter introduces the details, attempting to avoid any dependence on past logic programming experience. *)
 
 
 (** * Introducing Logic Programming *)