\documentclass{article}
\usepackage{a4wide,ot1patch}
\usepackage[latin1]{inputenc}
\usepackage{multicol}
\usepackage{charter}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{fancyheadings}

\addtolength{\oddsidemargin}{-6mm}
\addtolength{\evensidemargin}{-6mm}
\addtolength{\textwidth}{11mm}
\addtolength{\columnsep}{3mm}
\addtolength{\textheight}{8mm}
\addtolength{\topmargin}{-7.5mm}

\pagestyle{fancyplain}
\lhead[\fancyplain{}{A}]{\fancyplain{}{}}
\rhead[\fancyplain{}{C}]{\fancyplain{}{}}
\renewcommand{\headrulewidth}{0pt}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}


\begin{center}
\begin{tabular}{c}
\\[-5mm]
\LARGE\bf Novel Certified Parsers\\[-10mm]
\mbox{}
\end{tabular}
\end{center}
\thispagestyle{empty}
\mbox{}\\[-5mm]

\begin{multicols}{2}
\section*{Background}

\noindent
Parsers transform plain text into some abstract structure that can be analyzed by
computers for further processing.  One might think that parsers have been
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 real practical need for new results: for example the future HTML5 
Standard abandons a well-defined grammar specification, in favour of a bespoke
parser given as pseudo code. Proving any property about this parser is nearly 
impossible.

This work targets parsers from a certification point of view. Increasingly,
parsers are part of certified compilers, like
\mbox{\emph{CompCert}}~\cite{Leroy09}, which are guaranteed to be
bug-free. Such certified compilers are crucial in areas where software just
cannot fail. However, so far the parsers of these compilers have been left out
of the certification.  This is because parsing algorithms are often ad hoc and
their semantics is not clearly specified. This means, unfortunately, parsers
can harbour errors that potentially invalidate the whole certification and
correctness of the compiler. In this project, we aim to change this situation
with the help of the theorem prover Isabelle/HOL.

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 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
reasoned about entirely in terms regular expressions, which can be easily
represented in theorem provers. This work uses the device of derivatives of
regular expressions. We like to extend this device to parsers and grammars.
The aim is to come up with elegant and practical useful parsing algorithms
whose correctness can be certified in Isabelle/HOL.


\section*{Proposed Work}

A recent development in the field of parsing are Parsing Expression Grammars
(PEGs)~\cite{Ford04}, which
are an extension of the well-known Context Free Grammars
(CFGs). This extension introduces new regular operators, such as
negation and conjunction, on the right-hand side of grammar rules, as well as
priority orderings for rules. With these extensions, PEG parsing becomes much
more powerful and more useful in practice. For example disambiguation, formerly expressed by semantic
filters, can now be expressed directly using grammar rules. 

However, there is a serious limitation of PEGs, which affects potential
applications: grammars involving left recursion are not
allowed~\cite{Ford02}. Although one PEG parsing algorithm has already been
proposed that can deal with left recursion~\cite{WarthDM08}, there
is no correctness proof for it, not even one with ``pencil and paper''. One aim of this
research is to solve this sorry state-of-affairs by either certifying this
algorithm or inventing a new one. For this we will first devise a
fixed-point semantics of PEGs, against which we can certify a parser. For this
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
paper~\cite{KountouriotisNR09} gives a fixed-point semantics 
for negation operators, but not to the Kleene star.

For our 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
into a normal form. This transformation may potentially lead to rule explosion
and hence inefficient parsing. We will investigate whether this transformation
can be avoided.  The problem with Early-style parsers is that they need to be 
extended to PEG parsing in order to be helpful for us.


Finally, we want to investigate whether derivatives of regular expressions
~\cite{Brzozowski64,Might11,OwensReppyTuron09}
can be generalised to PEG parsing. In earlier work, we showed that lexing based on
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 addressed is again how to deal with 
left-recursive grammar rules.



\bibliography{Journal/document/root}
\bibliographystyle{abbrv}
\end{multicols}

%  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  \noindent {\bf Objectives:} The overall goals of the project are as follows:
%  \begin{itemize}
%  \item To solve the POPLmark challenge.

%  \item To complete and greatly improve the existing implementation of the
%    nominal datatype package.
%  \item To explore the strengths of this package by proving the
%    safety of SML.
%  \item To provide a basis for extracting programs from safety proofs.

%  \item To make the nominal datatype package usable for teaching
%    students about the lambda-calculus and the theory of programming
%    languages. \smallskip
%  \end{itemize}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% TeX-command-default: "PdfLaTeX"
%%% TeX-view-style: (("." "kpdf %s.pdf"))
%%% End: