--- a/cfp.tex	Mon Dec 01 15:05:37 2014 +0000
+++ b/cfp.tex	Mon Jan 26 12:32:49 2015 +0000
@@ -48,7 +48,7 @@
 Tobias Nipkow, \emph{TU M\"unchen}\\
 Michael Norrish, \emph{NICTA}\\
 Scott Owens, \emph{University of Kent}\\
-Randy Pollack, \emph{Havard University}\\
+Randy Pollack, \emph{Harvard University}\\
 Carsten Sch\"urmann, \emph{IT University of Copenhagen}\\
 Konrad Slind, \emph{Rockwell Collins}\\
 Alwen Tiu, \emph{Nanyang Technological University}\\
@@ -103,7 +103,7 @@
       verification, refinement, and synthesis for functional,
       declarative and imperative languages; formal semantics
       of programming languages; proof carrying code.
-\item Industrial application of theorem provers. 
+\item Industrial applications of theorem provers. 
 \item Formalization of mathematical theories. 
 \item Advances in theorem prover technology: proof automation
       and decision procedures, induction, combination of