\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]

\end{tabular}

\end{center}

\thispagestyle{empty}

\mbox{}\\[-5mm]

\begin{multicols}{2}

\section*{Background}

\noindent

Parsing is the act of transforming plain text into some

One might think that parsing has been studied to death and after

However recent results and novel approaches make it increasingly clear,

that this is not true anymore.

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 adhoc and their semantics

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 need to be formulated

in way so that it is easy to reason about them. In earlier work

precludes well-known algorithms working over graphs. However regular

regular expressions, which can be easily represented in theorem

expressions. We like to extend this device to parsers and grammars.

The aim is to come up with elegant and useful parsing algorithms

theorem prover.

\mbox{}\\[15cm]

%\small

%\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.

%    students about the lambda-calculus and the theory of programming

%    languages. \smallskip

%  \end{itemize}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\end{document}

%%% mode: latex

%%% TeX-master: t

%%% TeX-command-default: "PdfLaTeX"

%%% TeX-view-style: (("." "kpdf %s.pdf"))