\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 Certified Parsing\\[-10mm]
\mbox{}
\end{tabular}
\end{center}
\thispagestyle{empty}
\mbox{}\\[-5mm]

\begin{multicols}{2}
\section*{Background}
\noindent
Parsing is the act of transforming plain text into some
structure that can be analyzed by computers for further processing.
One might think that parsing has been studied to death and after
\emph{yacc} and \emph{lex} no new results can be obtained in this area.
However recent results and novel approaches make it increasingly clear,
that this is not true anymore.

We propose to approach the subject of parsing from a certification point
of view. Increasingly, parsers are part of certified compilers, like \mbox{\emph{CompCert}},
which are guaranteed to be correct and 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. Unfortunately, this means parsers can harbour
errors that potentially invalidate the whole certification and correctness
of the compiler. In this project, we like to change that.

Only in the last few years, theorem provers have become good enough
for establishing the correctness of some standard lexing and
parsing algorithms. For this, the algorithms still need to be formulated
in way so that it is easy to reason about them. In our earlier work
about lexing and regular languages, the authors showed that this
precludes well-known algorithms based automata. However we showed 
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 a
theorem prover.

\section*{Proposed Work}

A recent development in parsing is Parsing Expression Grammars (PEG), which
are an extension of the standard Context Free Grammars
(CFG)~\cite{Ford04a}. The extension introduces new regular operators, such as
negation and conjunction, on the right-hand sides of grammar rules, as well as
priority orderings on rules. With these extensions, PEG parsing becomes much
more powerful. For example disambiguation, formerly expressed by semantic
filters, can now be expressed directly using grammar rules. This means a
simpler and more systematic treatment of ambiguity and more concise grammar
specifications for programming languages.

However, a serious disadvantage of PEG is that it does not allow left
recursion, because parsing algorithms for PEG~\cite{Ford02b} can not deal with
left recursions. Although a new PEG parsing algorithm has been proposed
that can deal with left recursion~\cite{conf/pepm/WarthDM08}, there is no
correctness proof, not even in ``paper-and-pencil'' form. 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 formalize a fixed
point semantics of PEG, based on which an efficient, certified parsing
algorithm can be given given.

There are several existing works we can draw upon:
\begin{enumerate}
\item The works on PEG.
  \begin {enumerate}
  \item An operation semantics for PEG has already been given
    in~\cite{Ford04a}, but it is not adequate to deal with left recursions. But this
    work gives at least a precise description of what the original PEG meant
    for. This will serve an a basis to show the conservativeness of
    the fixed point semantics we are
    going to develop.
    
  \item The new algorithm~\cite{conf/pepm/WarthDM08} which claimed to be able
    to deal with left recursions. Although there is no correctness proof yet, this
    may provide some useful inspirations for our new algorithm design.
  \end{enumerate}

\item The works on Boolean Grammars~\cite{Okhotin/04a}. Boolean Grammar is
  very closely related to PEG, because it also contains negative and conjunctive
  grammars. The main differences are: First, Boolean Grammar has no ordering on
  productions; Second: Boolean Grammar does not contain STAR operator. There are
  two works about Boolean Grammar which might be useful for this research:
  
  \begin{enumerate}
  \item A fixed point semantics for Boolean
    Grammar~\cite{journals/iandc/KountouriotisNR09}. The idea to define the
    semantics of negative and conjunctive operators is certainly what we can
    borrow. Therefore, this work gives the basis on which we can add in production
    ordering and STAR operator.

  \item A parsing algorithm for Boolean Grammar based on CYK
    parsing~\cite{journals/iandc/KountouriotisNR09}. The draw back of CYK parsing
    is that: the original grammar specification needs to be transformed into a
    normal form. This transformation may lead to grammar explosion and is
    undesirable. One aim of this research is to see whether this transformation
    can be avoided. For this purpose, other parsing style may provide useful inspirations, for example:

    \begin{enumerate}
    \item Derivative
      Parsing~\cite{Brzozowski64,Almeidaetal10,OwensReppyTuron09,journals/corr/abs-1010-5023}. Christian
      Urban has used derivative methods to establish the correctness of a regular
      expression matcher, as well the the finite partition property of regular
      expression~\cite{WuZhangUrban11}.  There are well founded envisage that the
      derivative methods may provide the foundation to the new parsing algorithms of PEG.

    \item Early parsing~\cite{Earley70,AycHor02}. It is a refinement of CYK
      parsing which does not require the transformation to normal forms, and
      therefore provide one possible direction to adapt the current CYK based
      parsing algorithm of Boolean Grammar for PEG grammar.

    \item The new parsing algorithm proposed by Tom Ridge[???]. Recently,
      T. Ridge has proposed and certified an combinator style parsing algorithm for
      CFG, which borrows some ideas from Early parsing. The proposed algorithm is
      very simple and elegant. We are going to strive for a parsing algorithm as elegant as this one.
    \end{enumerate}
    
    Which of the above possibilities will finally get into our final solutions
    is an interesting point about this current research.

  \end{enumerate}
\end{enumerate}

Based on these works, we are quite confident that our idea may lead to some concrete results.

\mbox{}\\[15cm]

\noindent



\small
\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: