--- a/csupp.tex	Tue Sep 06 02:35:10 2011 +0000
+++ b/csupp.tex	Tue Sep 06 02:48:51 2011 +0000
@@ -25,7 +25,7 @@
 \begin{center}
 \begin{tabular}{c}
 \\[-5mm]
-\LARGE\bf Certified Parsing\\[-10mm]
+\LARGE\bf Novel Certified Parsers\\[-10mm]
 \mbox{}
 \end{tabular}
 \end{center}
@@ -41,7 +41,7 @@
 studied to death, and after \emph{yacc} and \emph{lex} no new results can be
 obtained in this area.  However recent developments and novel approaches make
 it increasingly clear, that this is not true anymore~\cite{Might11}. And
-there is a practical need for new results: for example the future HTML 5 
+there is a real practical need for new results: for example the future HTML 5 
 Standard abandons a well-defined grammar specification, in favour of a bespoke
 parser given as pseudo code.
 
@@ -58,7 +58,7 @@
 
 Only in the last few years, theorem provers have become powerful enough for
 establishing the correctness of some standard lexing and parsing
-algorithms. For this, the algorithms still need to be formulated in way so
+algorithms. For this, the algorithms still need to be formulated in a way so
 that it is easy to reason about them. In our earlier work about lexing and
 regular languages, we showed that this precludes well-known algorithms based
 automata~\cite{WuZhangUrban11}. However we showed also that regular languages can be formulated and
@@ -91,12 +91,12 @@
 semantics we take as starting point the paper~\cite{Ford04}, which does not
 treat left-recursion, but gives an operational semantics for PEG
 parsing. There are also good indications that we can adapt work on Boolean
-Grammars~\cite{Okhotin04}, which are similar to PEGs, and for which the
+Grammars~\cite{Okhotin04}, which are similar to PEGs and for which the
 paper~\cite{KountouriotisNR09} gives a fixed-point semantics 
 to negation operators, but not to the Kleene star.
 
-For the parsing algorithm, we might be able to draw inspiration from parsers
-based on the classic Cocke-Younger-Kasami (CYK)
+For the parsing algorithm, we might be able to build upon
+the classic Cocke-Younger-Kasami (CYK)
 algorithms~\cite{KountouriotisNR09} and
 Early~\cite{AycHor02, Earley70} parsers. The defect of CYK algorithms, however,
 is that the grammar specifications given by the user need to be transformed
@@ -112,8 +112,8 @@
 derivatives gives rise to very elegant regular expression matchers that can be
 certified in a theorem prover with ease.  We will study whether the idea of
 taking a derivative of a regular expression can be extended to rules in
-grammars. The problem that needs to be overcome is again how to deal with possible
-left-recursion in grammar rules.
+grammars. The problem that needs to be addressed is again how to deal with 
+left-recursive grammar rules.