\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:+
−