# HG changeset patch
# User urbanc
# Date 1315277331 0
# Node ID 86a4182c73e7bf2a58f65b2b212ea7b1aebe6226
# Parent  093e45c44d911eb40778733a58962ef4ca36ec53
more tuning on the proposal

diff -r 093e45c44d91 -r 86a4182c73e7 Journal/document/root.bib
--- a/Journal/document/root.bib	Tue Sep 06 02:35:10 2011 +0000
+++ b/Journal/document/root.bib	Tue Sep 06 02:48:51 2011 +0000
@@ -254,6 +254,8 @@
 
 
 
+
+
 @Article{Okhotin04,
   author =	"A.~Okhotin",
   title =	"{B}oolean {G}rammars",
@@ -268,30 +270,30 @@
   title =	"{W}ell-founded {S}emantics for {B}oolean {G}rammars",
   author =	"V.~Kountouriotis and C.~Nomikos and P.~Rondogiannis",
   journal =	"Information and Computation",
-  year = 	2009,
-  number =	9,
-  volume =	207,
-  pages     =   {945--967}
+  year = 	"2009",
+  number =	"9",
+  volume =	"207",
+  pages     =   "945--967"
 }
 
 
 @article{Leroy09,
-  author = {X.~Leroy},
-  title = {{F}ormal {V}erification of a {R}ealistic {C}ompiler},
-  journal = {Communications of the ACM},
-  year = 2009,
-  volume = 52,
-  number = 7,
-  pages = {107--115}
+  author =      {X.~Leroy},
+  title =       {{F}ormal {V}erification of a {R}ealistic {C}ompiler},
+  journal =     {Communications of the ACM},
+  year =        {2009},
+  volume =      {52},
+  number =      {7},
+  pages =       {107--115}
 }
 
 
 @Unpublished{Might11,
   title =	"{Y}acc is {D}ead",
   author =	"M.~Might and D.~Darais",
-  note  = "To appear in {\it Proc.~of the 16th ACM International Conference on 
-           Functional Programming (ICFP)}",
-  year = 2011
+  note  =       "To appear in {\it Proc.~of the 16th ACM International Conference on 
+                 Functional Programming (ICFP)}",
+  year =        "2011"
 }
 
 @InProceedings{Ford04,
@@ -299,7 +301,7 @@
   title =	"{P}arsing {E}xpression {G}rammars: {A} {R}ecognition-{B}ased
 		 {S}yntactic {F}oundation",
   booktitle =	"Proc.~of the 31st ACM Symposium on Principles of Programming Languages (POPL)",
-  year = 	2004,
+  year = 	"2004",
   pages =	"111--122"
 }
 
@@ -309,12 +311,12 @@
                  ({F}unctional {P}earl)",
   booktitle =	"Proc.~of the 7th ACM International Conference on Functional Programming (ICFP)",
   year = 	"2002",
-  pages  = {36--47}
+  pages  =      "36--47"
 
 }
 
 @InProceedings{WarthDM08,
-  title =	"{{P}ackrat {P}arsers {C}an {S}upport {L}eft {R}ecursion}",
+  title =	"{P}ackrat {P}arsers {C}an {S}upport {L}eft {R}ecursion",
   author =	"A.~Warth and J.~R.~Douglass and T.~D.~Millstein",
   booktitle =	"Proc. of the {ACM} Symposium on
 		 Partial Evaluation and Semantics-based Program
@@ -324,18 +326,18 @@
 }
 
 @Article{Earley70,
-  author =	"J. Earley",
-  title =	"{An Efficient Context-Free Parsing Algorithm}",
+  author =	"J.~Earley",
+  title =	"{A}n {E}fficient {C}ontext-{F}ree {P}arsing {A}lgorithm",
   journal =	"Communications of the ACM",
   volume =	"13",
   number =	"2",
-  pages =       {94--102},
+  pages =       "94--102",
   year = 	"1970"
 }
 
 @Article{AycHor02,
   author =	"J.~Aycock and R.~N.~Horspool",
-  title =	"{{P}ractical {E}arley {P}arsing}",
+  title =	"{P}ractical {E}arley {P}arsing",
   journal =	"The Computer Journal",
   volume =	"45",
   number =      "6",
diff -r 093e45c44d91 -r 86a4182c73e7 csupp.pdf
Binary file csupp.pdf has changed
diff -r 093e45c44d91 -r 86a4182c73e7 csupp.tex
--- 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.