1 \documentclass[11pt,a4paper]{article}

     2 \usepackage{isabelle,isabellesym}

     3 

     4 % this should be the last package used

     5 \usepackage{pdfsetup}

     6 

     7 % urls in roman style, theory text in math-similar italics

     8 \urlstyle{rm}

     9 \isabellestyle{it}

    10 

    11 

    12 \begin{document}

    13 

    14 \title{POSIX Lexing with Derivatives of Regular Expressions}

    15 \author{Fahad Ausaf \and Roy Dyckhoff \and Christian Urban}

    16 \maketitle

    17 

    18 \begin{abstract}

    19   Brzozowski introduced the notion of derivatives for regular

    20   expressions. They can be used for a very simple regular expression

    21   matching algorithm. Sulzmann and Lu \cite{Sulzmann2014} cleverly extended this algorithm

    22   in order to deal with POSIX matching, which is the underlying

    23   disambiguation strategy for regular expressions needed in

    24   lexers. In this entry we give our inductive definition

    25   of what a POSIX value is and show (i) that such a value is unique (for

    26   given regular expression and string being matched) and (ii) that

    27   Sulzmann and Lu's algorithm always generates such a value (provided

    28   that the regular expression matches the string). We also prove the

    29   correctness of an optimised version of the POSIX matching

    30   algorithm. 

    31 \end{abstract}

    32 

    33 \tableofcontents

    34 

    35 % include generated text of all theories

    36 \input{session}

    37 

    38 \bibliographystyle{abbrv}

    39 \bibliography{root}

    40 

    41 \end{document}