--- a/latex/cpdt.bib	Sun Apr 22 15:38:11 2012 -0400
+++ b/latex/cpdt.bib	Sun Apr 22 15:51:03 2012 -0400
@@ -375,3 +375,42 @@
  publisher = {Springer-Verlag},
  address = {London, UK, UK},
 } 
+
+@article{continuations,
+ author = {Reynolds, John C.},
+ title = {The discoveries of continuations},
+ journal = {Lisp Symb. Comput.},
+ issue_date = {Nov. 1993},
+ volume = {6},
+ number = {3-4},
+ month = nov,
+ year = {1993},
+ issn = {0892-4635},
+ pages = {233--248},
+ numpages = {16},
+ url = {http://dx.doi.org/10.1007/BF01019459},
+ doi = {10.1007/BF01019459},
+ acmid = {198114},
+ publisher = {Kluwer Academic Publishers},
+ address = {Hingham, MA, USA},
+ keywords = {continuation, continuation-passing style, semantics},
+}
+
+@article{unification,
+ author = {Robinson, J. A.},
+ title = {A Machine-Oriented Logic Based on the Resolution Principle},
+ journal = {J. ACM},
+ issue_date = {Jan. 1965},
+ volume = {12},
+ number = {1},
+ month = jan,
+ year = {1965},
+ issn = {0004-5411},
+ pages = {23--41},
+ numpages = {19},
+ url = {http://doi.acm.org/10.1145/321250.321253},
+ doi = {10.1145/321250.321253},
+ acmid = {321253},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+}

--- a/src/Match.v	Sun Apr 22 15:38:11 2012 -0400
+++ b/src/Match.v	Sun Apr 22 15:51:03 2012 -0400
@@ -471,7 +471,7 @@
 
    Even basic [idtac] is an embedded imperative program, so we may not automatically mix it with purely functional code.  In fact, a semicolon operator alone marks a span of Ltac code as an embedded tactic script.  This makes some amount of sense, since pure functional languages have no need for sequencing: since they lack side effects, there is no reason to run an expression and then just throw away its value and move on to another expression.
 
-   The solution is like in Haskell: we must %``%#"#monadify#"#%''% our pure program to give it access to side effects.  The trouble is that the embedded tactic language has no [return] construct.  Proof scripts are about proving theorems, not calculating results.  We can apply a somewhat awkward workaround that requires translating our program into %\index{continuation-passing style}\emph{%#<i>#continuation-passing style#</i>#%}%, a program structuring idea popular in functional programming. *)
+   The solution is like in Haskell: we must %``%#"#monadify#"#%''% our pure program to give it access to side effects.  The trouble is that the embedded tactic language has no [return] construct.  Proof scripts are about proving theorems, not calculating results.  We can apply a somewhat awkward workaround that requires translating our program into %\index{continuation-passing style}\emph{%#<i>#continuation-passing style#</i>#%}~\cite{continuations}%, a program structuring idea popular in functional programming. *)
 
 (* begin hide *)
 Reset length.

--- a/src/Predicates.v	Sun Apr 22 15:38:11 2012 -0400
+++ b/src/Predicates.v	Sun Apr 22 15:51:03 2012 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2011, Adam Chlipala
+(* Copyright (c) 2008-2012, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -892,7 +892,7 @@
   intros; eapply even_contra'; eauto.
 Qed.
 
-(** We use a variant %\index{tactics!apply}%[eapply] of [apply] which has the same relationship to [apply] as [eauto] has to [auto].  An invocation of [apply] only succeeds if all arguments to the rule being used can be determined from the form of the goal, whereas [eapply] will introduce unification variables for undetermined arguments.  In this case, [eauto] is able to determine the right values for those unification variables.
+(** We use a variant %\index{tactics!apply}%[eapply] of [apply] which has the same relationship to [apply] as [eauto] has to [auto].  An invocation of [apply] only succeeds if all arguments to the rule being used can be determined from the form of the goal, whereas [eapply] will introduce unification variables for undetermined arguments.  In this case, [eauto] is able to determine the right values for those unification variables, using (unsurprisingly) a variant of the classic algorithm for %\emph{%#<i>#unification#</i>#%}~\cite{unification}%.
 
 By considering an alternate attempt at proving the lemma, we can see another common pitfall of inductive proofs in Coq.  Imagine that we had tried to prove [even_contra'] with all of the [forall] quantifiers moved to the front of the lemma statement. *)
 

--- a/src/StackMachine.v	Sun Apr 22 15:38:11 2012 -0400
+++ b/src/StackMachine.v	Sun Apr 22 15:51:03 2012 -0400
@@ -814,7 +814,7 @@
 Lemma tcompile_correct' : forall t (e : texp t) ts (s : vstack ts),
   tprogDenote (tcompile e ts) s = (texpDenote e, s).
 
-(** While lemma [compile_correct'] quantified over a program that is the %``%#"#continuation#"#%''% for the expression we are considering, here we avoid drawing in any extra syntactic elements.  In addition to the source expression and its type, we also quantify over an initial stack type and a stack compatible with it.  Running the compilation of the program starting from that stack, we should arrive at a stack that differs only in having the program's denotation pushed onto it.
+(** While lemma [compile_correct'] quantified over a program that is the %``%#"#continuation#"#%''~\cite{continuations}% for the expression we are considering, here we avoid drawing in any extra syntactic elements.  In addition to the source expression and its type, we also quantify over an initial stack type and a stack compatible with it.  Running the compilation of the program starting from that stack, we should arrive at a stack that differs only in having the program's denotation pushed onto it.
 
    Let us try to prove this theorem in the same way that we settled on in the last section. *)