diff -r 47179a172c54 -r 16af5b8bd285 thys/Journal/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Journal/document/root.tex	Sun Feb 26 23:46:22 2017 +0000
@@ -0,0 +1,79 @@
+\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}
+
+\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}$}}
+
+\def\Brz{Brzozowski}
+\def\der{\backslash}
+\newtheorem{falsehood}{Falsehood}
+\newtheorem{conject}{Conjecture}
+
+\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{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.
+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
+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 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 and
+explain why the gaps in this argument cannot be filled easily.\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: