--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Journal/document/root.tex	Mon Nov 01 10:40:21 2021 +0000
@@ -0,0 +1,101 @@
+\documentclass[runningheads]{llncs}
+\usepackage{times}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{mathpartir}
+\usepackage{tikz}
+\usepackage{pgf}
+\usetikzlibrary{positioning}
+\usepackage{pdfsetup}
+\usepackage{stmaryrd}
+\usepackage{url}
+\usepackage{color}
+\usepackage[safe]{tipa}
+\usepackage[sc]{mathpazo}
+\usepackage{fontspec}
+%\setmainfont[Ligatures=TeX]{Palatino Linotype}
+
+
+\titlerunning{POSIX Lexing with Derivatives of Regular Expressions}
+
+\urlstyle{rm}
+\isabellestyle{it}
+\renewcommand{\isastyleminor}{\it}% 
+\renewcommand{\isastyle}{\normalsize\it}%
+
+
+\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+\renewcommand{\isasymiota}{\makebox[0mm]{${}^{\prime}$}}
+\renewcommand{\isasymin}{\ensuremath{\,\in\,}}
+
+
+\def\Brz{Brzozowski}
+\def\der{\backslash}
+\newtheorem{falsehood}{Falsehood}
+\newtheorem{conject}{Conjecture}
+
+\begin{document}
+\renewcommand{\thefootnote}{$\star$} \footnotetext[1]{This paper is a
+  revised and expanded version of \cite{AusafDyckhoffUrban2016}.
+  Compared with that paper we give a second definition for POSIX
+  values introduced by Okui Suzuki \cite{OkuiSuzuki2010,OkuiSuzukiTech}
+  and prove that it is
+  equivalent to our original one. This
+  second definition is based on an ordering of values and very similar to,
+  but not equivalent with, the
+  definition given by Sulzmann and Lu~\cite{Sulzmann2014}.
+  The advantage of the definition based on the
+  ordering is that it implements more directly the informal rules from the
+  POSIX standard.
+  We also prove Sulzmann \& Lu's conjecture that their bitcoded version
+  of the POSIX algorithm is correct. Furthermore we extend our results to additional constructors of regular
+  expressions.}  \renewcommand{\thefootnote}{\arabic{footnote}}
+
+
+\title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions}
+\author{Fahad Ausaf\inst{1} \and Roy Dyckhoff\inst{2} \and Christian Urban\inst{3}}
+\institute{King's College London\\
+		\email{fahad.ausaf@icloud.com}
+\and University of St Andrews\\
+		\email{roy.dyckhoff@st-andrews.ac.uk}
+\and King's College London\\
+		\email{christian.urban@kcl.ac.uk}}
+\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 cleverly extended this algorithm
+in order to deal with POSIX matching, which is the underlying
+disambiguation strategy for regular expressions needed in lexers.
+Their algorithm generates POSIX values which encode the information of
+\emph{how} a regular expression matches a string---that is, which part
+of the string is matched by which part of the regular expression.  In
+this paper 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 show that $(iii)$ our inductive
+definition of a POSIX value is equivalent to an alternative definition
+by Okui and Suzuki which identifies POSIX values as least elements
+according to an ordering of values.  We also prove the correctness of
+Sulzmann's bitcoded version of the POSIX matching algorithm and extend the
+results to additional constructors for regular expressions.  \smallskip
+
+{\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,
+Isabelle/HOL
+\end{abstract}
+
+\input{session}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: