--- a/thys3/document/root.tex Wed Oct 12 14:08:06 2022 +0100
+++ b/thys3/document/root.tex Wed Oct 12 15:23:42 2022 +0100
@@ -1,4 +1,5 @@
-\documentclass[runningheads]{lipics-v2021}
+\documentclass[runningheads]{llncs}
+%!\documentclass[runningheads]{lipics-v2021}
\usepackage{times}
\usepackage{isabelle}
\usepackage{isabellesym}
@@ -10,7 +11,7 @@
\usetikzlibrary{positioning}
%\usepackage{pdfsetup}
\usepackage{stmaryrd}
-%\usepackage{url}
+\usepackage{url}
%\usepackage{color}
%\usepackage[safe]{tipa}
%\usepackage[sc]{mathpazo}
@@ -58,20 +59,24 @@
\newtheorem{falsehood}{Falsehood}
\newtheorem{conject}{Conjecture}
-\bibliographystyle{plainurl}
+%!\bibliographystyle{plainurl}
+\bibliographystyle{plain}
\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}{}{}
-\authorrunning{C.~Tan and C.~Urban}
-\keywords{POSIX matching and lexing, derivatives of regular expressions, Isabelle/HOL}
-\category{}
-\ccsdesc[100]{Design and analysis of algorithms}
-\ccsdesc[100]{Formal languages and automata theory}
-\Copyright{\mbox{}}
-\renewcommand{\DOIPrefix}{}
-\nolinenumbers
+\author{Chengsong Tan\inst{1,2} \and Christian Urban\inst{2}}
+\institute{Imperial College London \and King's College London\\
+\email{\{chengsong.tan,christian.urban\}@kcl.ac.uk}}
+%!\author{Chengsong Tan}{King's College London}{chengsong.tan@kcl.ac.uk}{}{}
+%!\author{Christian Urban}{King's College London}{christian.urban@kcl.ac.uk}{}{}
+%!\authorrunning{C.~Tan and C.~Urban}
+%!\keywords{POSIX matching and lexing, derivatives of regular expressions, Isabelle/HOL}
+%!\category{}
+%!\ccsdesc[100]{Design and analysis of algorithms}
+%!\ccsdesc[100]{Formal languages and automata theory}
+%!\Copyright{\mbox{}}
+%!\renewcommand{\DOIPrefix}{}
+%!\nolinenumbers
\begin{document}
@@ -93,9 +98,10 @@
paper we describe a variant of Sulzmann and Lu's algorithm: Our
variant is a recursive functional program, whereas Sulzmann
and Lu's version involves a fixpoint construction. We \textit{(i)}
- prove in Isabelle/HOL that our algorithm is correct and generates
- unique POSIX values; we also \textit{(ii)} establish finite
- bounds for the size of the derivatives.
+ prove in Isabelle/HOL that our variant is correct and generates
+ unique POSIX values (no such proof has been given for the
+ original algorithm by Sulzmann and Lu); we also \textit{(ii)} establish finite
+ bounds for the size of our derivatives.
%The size can be seen as a
%proxy measure for the efficiency of the lexing algorithm: because of