--- a/thys/Paper/document/root.tex Sun Feb 28 14:01:12 2016 +0000
+++ b/thys/Paper/document/root.tex Tue Mar 01 12:10:11 2016 +0000
@@ -1,4 +1,5 @@
\documentclass[runningheads]{llncs}
+\usepackage{times}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
@@ -8,16 +9,15 @@
\usepackage{pgf}
\usepackage{pdfsetup}
\usepackage{ot1patch}
-\usepackage{times}
\usepackage{stmaryrd}
\usepackage{url}
\usepackage{color}
-\titlerunning{BLA BLA}
+\titlerunning{POSIX Lexing with Derivatives}
\urlstyle{rm}
\isabellestyle{it}
-\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastyleminor}{\it}%
\renewcommand{\isastyle}{\normalsize\it}%
@@ -28,25 +28,31 @@
\definecolor{mygrey}{rgb}{.80,.80,.80}
\def\Brz{Brzozowski}
-
+\def\der{\backslash}
+\newcommand{\eps}{\varepsilon}
+\newcommand{\mts}{\eps}
\begin{document}
\title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions (Proof Pearl)}
-\author{Fahad Ausaf\inst{1} \and Roy Dyckhoff\inst{2} \and Christian Urban\inst{1}}
-\institute{King's College London, United Kingdom \and
- St Andrews}
+\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}
-\Brz{} introduced the notion of derivatives for regular
+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. Sulzmann and Lu have made available on-line what they call a
-``rigorous proof'' of the correctness of their algorithm w.r.t.~their
+disambiguation strategy for regular expressions needed in lexers.
+Sulzmann and Lu have made available on-line what they call a
+``rigorous proof'' of the correctness of their algorithm w.r.t.\ their
specification; regrettably, it appears to us to have unfillable gaps.
In the first part of this paper we give our inductive definition of
what a POSIX value is and show $(i)$ that such a value is unique (for
@@ -55,10 +61,10 @@
that the regular expression matches the string). We also prove the
correctness of an optimised version of the POSIX matching
algorithm. Our definitions and proof are much simpler than those by
-Sulzmann and Lu and can be easily formalised in Isabelle/HOL. In the
-second part we analyse the correctness argument by Sulzmann and Lu in
-more detail and explain why it seems hard to turn it into a proof
-rigorous enough to be accepted by a system such as Isabelle/HOL.
+Sulzmann and Lu and can be easily formalised in Isabelle/HOL. In the
+second part we analyse the correctness argument by Sulzmann and Lu and
+explain why it seems hard to turn it into a proof rigorous enough to
+be accepted by a system such as Isabelle/HOL.\smallskip
{\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,
Isabelle/HOL