Finished last pass through the book before beginning the MIT Press editorial process

latex/cpdt.bib

@@ -73,6 +73,7 @@
     title =        {{seL4}: Formal Verification of an {OS} Kernel},
     booktitle =    {Proceedings of the 22nd {ACM Symposium on Operating Systems Principles}},
     year =         {2009},
+    pages =        {207--220}
 }
 
 @Book{Isabelle/HOL,
@@ -113,6 +114,7 @@
   title = {Inductive Definitions in the System {Coq} - Rules and Properties},
   year = {1993},
   booktitle = {Proceedings of the International Conference on {Typed Lambda Calculi and Applications}},
+  pages = {328--345}
 }
 
 @inproceedings{SetsInTypes,
@@ -120,6 +122,7 @@
   title     = {Sets in Types, Types in Sets},
   booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software},
   year      = {1997},
+  pages     = {530--546}
 }
 
 @article{CoC,
@@ -133,8 +136,9 @@
 @inproceedings{GADT,
   author = {Hongwei Xi and Chiyan Chen and Gang Chen},
   title = {Guarded Recursive Datatype Constructors},
-  booktitle = {Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages},
-  year = {2003}
+  booktitle = {Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+  year = {2003},
+  pages = {224--235}
 }
 
 @article{Curry,
@@ -162,7 +166,7 @@
  title = {Higher-order abstract syntax},
  booktitle = {Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation},
  year = {1988},
-% pages = {199--208},
+ pages = {199--208}
 } 
 
 @article{HOU,
@@ -187,6 +191,7 @@
  title = {The essence of functional programming},
  booktitle = {Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  year = {1992},
+ pages = {1--14}
 } 
 
 @inproceedings{IO,
@@ -194,13 +199,15 @@
  title = {Imperative functional programming},
  booktitle = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  year = {1993},
+ pages = {71--84}
 } 
 
 @InProceedings{separation,
   author = 	 {John C. Reynolds},
   title = 	 {Separation Logic: A Logic for Shared Mutable Data Structures},
   booktitle =    {Proceedings of the IEEE Symposium on Logic in Computer Science},
-  year = 	 {2002}
+  year = 	 {2002},
+  pages =        {55--74}
 }
 
 @article{Okasaki,
@@ -235,6 +242,7 @@
  title = {Proof-carrying code},
  booktitle = {Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  year = {1997},
+ pages = {106--119}
 }
 
 @inproceedings{XCAP,
@@ -242,6 +250,7 @@
  title = {Certified assembly programming with embedded code pointers},
  booktitle = {Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  year = {2006},
+ pages = {320--333}
  }
 
 @TechReport{IT,
@@ -257,7 +266,8 @@
  author = {Xavier Leroy and Herv\'e Grall},
  title = {Coinductive big-step operational semantics},
  year = {2006},
- booktitle = {Proceedings of the 15th European Symposium on Programming}
+ booktitle = {Proceedings of the 15th European Symposium on Programming},
+ pages = {54--68}
 }
 
 @InBook{WinskelDomains,
@@ -300,7 +310,7 @@
  title = {How to make ad-hoc polymorphism less ad hoc},
  booktitle = {Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  year = {1989},
-% pages = {60--76},
+ pages = {60--76}
 } 
 
 @inproceedings{reflection,
@@ -308,6 +318,7 @@
   title     = {Using reflection to build efficient and certified decision procedures},
   booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software},
   year      = {1997},
+  pages     = {515--529}
 }
 
 @inproceedings{JMeq,
@@ -359,6 +370,7 @@ author = {Adam Chlipala},
 title = {A Verified Compiler for an Impure Functional Language},
 booktitle = {Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 year = {2010},
+pages = {93--106}
 }
 
 @inproceedings{Isar,
@@ -366,6 +378,7 @@ year = {2010},
  title = {Isar - A Generic Interpretative Approach to Readable Formal Proof Documents},
  booktitle = {Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics},
  year = {1999},
+ pages = {167--184}
 } 
 
 @article{continuations,

src/Conclusion.v

@@ -9,7 +9,7 @@
 
 (** %\addcontentsline{toc}{chapter}{Conclusion}\chapter*{Conclusion}% *)
 
-(** I have designed this book to present the key ideas needed to get started with productive use of Coq.  Many people have learned to use Coq through a variety of resources, yet there is a distinct lack of agreement on structuring principles and techniques for easing the evolution of Coq developments over time.  Here I have emphasized two unusual techniques: programming with dependent types, and proving with scripted proof automation.  I have also tried to present other material following my own take on how to keep Coq code beautiful and scalable.
+(** I have designed this book to present the key ideas needed to get started with productive use of Coq.  Many people have learned to use Coq through a variety of resources, yet there is a distinct lack of agreement on structuring principles and techniques for easing the evolution of Coq developments over time.  Here I have emphasized two unusual techniques: programming with dependent types and proving with scripted proof automation.  I have also tried to present other material following my own take on how to keep Coq code beautiful and scalable.
 
    Part of the attraction of Coq and similar tools is that their logical foundations are small.  A few pages of %\LaTeX{}%#LaTeX# code suffice to define CIC, Coq's logic, yet there do not seem to be any practical limits on which mathematical concepts may be encoded on top of this modest base.  At the same time, the _pragmatic_ foundation of Coq is vast, encompassing tactics, libraries, and design patterns for programs, theorem statements, and proof scripts.  I hope the preceding chapters have given a sense of just how much there is to learn before it is possible to drive Coq with the same ease with which many readers write informal proofs!  The pay-off of this learning process is that many proofs, especially those with many details to check, become much easier to write than they are on paper.  Further, the truth of such theorems may be established with much greater confidence, even without reading proof details.
 

src/ProgLang.v

@@ -299,7 +299,7 @@ Module FirstOrder.
     induction e; pl.
   Qed.
 
-  (** The lemma statement is a mouthful, with all its details of typing contexts and substitutions.  It is usually prudent to state a final theorem in as simple a way as possible, to help your readers believe that you have proved what they expect.  We do that here for the simple case of terms with empty typing contexts. *)
+  (** The lemma statement is a mouthful, with all its details of typing contexts and substitutions.  It is usually prudent to state a final theorem in as simple a way as possible, to help your readers believe that you have proved what they expect.  We follow that advice here for the simple case of terms with empty typing contexts. *)
 
   Theorem unletSound : forall t (e : term nil t),
     termDenote (unlet e HNil) HNil = termDenote e HNil.
@@ -313,7 +313,7 @@ End FirstOrder.
 
 (** * Parametric Higher-Order Abstract Syntax *)
 
-(** In contrast to first-order encodings,%\index{higher-order syntax}% _higher-order_ encodings avoid explicit modeling of variable identity.  Instead, the binding constructs of an%\index{object language}% _object language_ (the language being formalized) can be represented using the binding constructs of the%\index{meta language}% _meta language_ (the language in which the formalization is done).  The best known higher-order encoding is called%\index{higher-order abstract syntax}\index{HOAS}% _higher-order abstract syntax_ (HOAS) %\cite{HOAS}%, and we can start by attempting to apply it directly in Coq. *)
+(** In contrast to first-order encodings,%\index{higher-order syntax}% _higher-order_ encodings avoid explicit modeling of variable identity.  Instead, the binding constructs of an%\index{object language}% _object language_ (the language being formalized) can be represented using the binding constructs of the%\index{meta language}% _meta language_ (the language in which the formalization is done).  The best known higher-order encoding is called%\index{higher-order abstract syntax}% _higher-order abstract syntax_ (HOAS) %\cite{HOAS}%, and we can start by attempting to apply it directly in Coq. *)
 
 Module HigherOrder.
 
@@ -332,7 +332,7 @@ Module HigherOrder.
 
    However, Coq rejects this definition for failing to meet the %\index{strict positivity requirement}%strict positivity restriction.  For instance, the constructor [Abs] takes an argument that is a function over the same type family [term] that we are defining.  Inductive definitions of this kind can be used to write non-terminating Gallina programs, which breaks the consistency of Coq's logic.
 
-   An alternate higher-order encoding is%\index{parametric higher-order abstract syntax}\index{PHOAS}% _parametric HOAS_, as introduced by Washburn and Weirich%~\cite{BGB}% for Haskell and tweaked by me%~\cite{PhoasICFP08}% for use in Coq.  Here the idea is to parameterize the syntax type by a type family standing for a _representation of variables_. *)
+   An alternate higher-order encoding is%\index{parametric higher-order abstract syntax}\index{PHOAS|see{parametric higher-order abstract syntax}}% _parametric HOAS_, as introduced by Washburn and Weirich%~\cite{BGB}% for Haskell and tweaked by me%~\cite{PhoasICFP08}% for use in Coq.  Here the idea is to parameterize the syntax type by a type family standing for a _representation of variables_. *)
 
   Section var.
     Variable var : type -> Type.
@@ -367,7 +367,7 @@ Module HigherOrder.
   Example three_the_hard_way : Term Nat := fun var =>
     App (App (add var) (Const 1)) (Const 2).
 
-  (** The argument [var] does not even appear in the function body for [add].  How can that be?  By giving our terms expressive types, we allow Coq to infer many arguments for us.  In fact, we do not even need to name the [var] argument!  Even though these formal parameters appear as underscores, they _are_ mentioned in the function bodies that type inference calculates. *)
+  (** The argument [var] does not even appear in the function body for [add].  How can that be?  By giving our terms expressive types, we allow Coq to infer many arguments for us.  In fact, we do not even need to name the [var] argument! *)
 
   Example add' : Term (Func Nat (Func Nat Nat)) := fun _ =>
     Abs (fun x => Abs (fun y => Plus (Var x) (Var y))).
@@ -375,6 +375,8 @@ Module HigherOrder.
   Example three_the_hard_way' : Term Nat := fun _ =>
     App (App (add' _) (Const 1)) (Const 2).
 
+  (** Even though the [var] formal parameters appear as underscores, they _are_ mentioned in the function bodies that type inference calculates. *)
+
 
   (** ** Functional Programming with PHOAS *)
 

src/Universes.v

@@ -371,7 +371,7 @@ Error: Impossible to unify "?35 = ?34" with "unit = unit".
 
 Coq tells us that we cannot, in fact, apply our lemma [symmetry] here, but the error message seems defective.  In particular, one might think that [apply] should unify [?35] and [?34] with [unit] to ensure that the unification goes through.  In fact, the issue is in a part of the unification problem that is _not_ shown to us in this error message!
 
-The following command is the secret to getting better error messages in such cases: *)
+The following command is the secret to getting better error messages in such cases:%\index{Vernacular commands!Set Printing All}% *)
 
   Set Printing All.
   (** %\vspace{-.15in}%[[