Pass over Match

latex/cpdt.bib

@@ -173,3 +173,32 @@
  year = {1973},
  pages = {257--267}
 }
+
+@InBook{TAPLNatDed,
+  author       = "Benjamin C. Pierce",
+  title        = "Types and Programming Languages",
+  year         = "2002",
+  publisher    = "MIT Press",
+  chapter      = "9.4"
+}
+
+@inproceedings{Monads,
+ author = {Wadler, Philip},
+ title = {The essence of functional programming},
+ booktitle = {Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+ year = {1992},
+} 
+
+@inproceedings{IO,
+ author = {Peyton Jones, Simon L. and Wadler, Philip},
+ title = {Imperative functional programming},
+ booktitle = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+ year = {1993},
+} 
+
+@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}
+}
\ No newline at end of file

src/StackMachine.v

@@ -505,7 +505,7 @@ Lemma compile_correct' : forall e s p, progDenote (compile e ++ p) s =
   induction e; crush.
 Qed.
 
-(** We need only to state the basic inductive proof scheme and call a tactic that automates the tedious reasoning in between.  In contrast to the period tactic terminator from our last proof, the %\index{tacticals!semicolon}%semicolon tactic separator supports structured, compositional proofs.  The tactic [t1; t2] has the effect of running [t1] and then running [t2] on each remaining subgoal.  The semicolon is one of the most fundamental building blocks of effective proof automation.  The period terminator is very useful for exploratory proving, where you need to see intermediate proof states, but final proofs of any serious complexity should have just one period, terminating a single compound tactic that probably uses semicolons.
+(** We need only to state the basic inductive proof scheme and call a tactic that automates the tedious reasoning in between.  In contrast to the period tactic terminator from our last proof, the %\index{tactics!semicolon}%semicolon tactic separator supports structured, compositional proofs.  The tactic [t1; t2] has the effect of running [t1] and then running [t2] on each remaining subgoal.  The semicolon is one of the most fundamental building blocks of effective proof automation.  The period terminator is very useful for exploratory proving, where you need to see intermediate proof states, but final proofs of any serious complexity should have just one period, terminating a single compound tactic that probably uses semicolons.
 
 The [crush] tactic comes from the library associated with this book and is not part of the Coq standard library.  The book's library contains a number of other tactics that are especially helpful in highly-automated proofs.