--- 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",
Binary file csupp.pdf has changed
--- 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.