\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}


\begin{document}

\title{POSIX Lexing with Derivatives of Regular Expressions}
\author{Fahad Ausaf \and Roy Dyckhoff \and Christian Urban}
\maketitle

\begin{abstract}
  Brzozowski introduced the notion of derivatives for regular
  expressions. They can be used for a very simple regular expression
  matching algorithm. Sulzmann and Lu \cite{Sulzmann2014} cleverly extended this algorithm
  in order to deal with POSIX matching, which is the underlying
  disambiguation strategy for regular expressions needed in
  lexers. In this entry we give our inductive definition
  of what a POSIX value is and show (i) that such a value is unique (for
  given regular expression and string being matched) and (ii) that
  Sulzmann and Lu's algorithm always generates such a value (provided
  that the regular expression matches the string). We also prove the
  correctness of an optimised version of the POSIX matching
  algorithm. 
\end{abstract}

\tableofcontents

% include generated text of all theories
\input{session}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}