--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Paper/document/root.tex	Tue Jan 25 13:12:50 2022 +0000
@@ -0,0 +1,88 @@
+\documentclass[runningheads]{lipics-v2021}
+\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}
+
+
+
+
+\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}
+
+\bibliographystyle{plainurl}
+
+\title{{POSIX} {L}exing with {B}itcoded {D}erivatives}
+\titlerunning{POSIX Lexing with Bitcoded Derivatives}
+\author{Chengsong Tan}{King's College London}{chengsong.tan@kcl.ac.uk}{}{}
+\author{Christian Urban}{King's College London}{christian.urban@kcl.ac.uk}{}{}
+
+
+\begin{document}
+\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: