thys/Paper/document/root.tex
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Thu, 25 Feb 2016 12:17:31 +0000
changeset 105 80218dddbb15
parent 95 a33d3040bf7e
child 107 6adda4a667b1
permissions -rwxr-xr-x
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
95
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
\documentclass[runningheads]{llncs}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     2
\usepackage{isabelle}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     3
\usepackage{isabellesym}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     4
\usepackage{amsmath}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     5
\usepackage{amssymb}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     6
\usepackage{mathpartir}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
\usepackage{tikz}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     8
\usepackage{pgf}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     9
\usepackage{pdfsetup}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    10
\usepackage{ot1patch}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    11
\usepackage{times}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    12
\usepackage{stmaryrd}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    13
\usepackage{url}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    14
\usepackage{color}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    15
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    16
\titlerunning{BLA BLA}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    17
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    18
\urlstyle{rm}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    19
\isabellestyle{it}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    20
\renewcommand{\isastyleminor}{\it}%
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    21
\renewcommand{\isastyle}{\normalsize\it}%
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    22
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    23
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    24
\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    25
\renewcommand{\isasymequiv}{$\dn$}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    26
\renewcommand{\isasymemptyset}{$\varnothing$}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    27
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    28
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    29
\definecolor{mygrey}{rgb}{.80,.80,.80}
105
80218dddbb15 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 95
diff changeset
    30
\def\Brz{Brzozowski}
80218dddbb15 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 95
diff changeset
    31
95
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    32
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    33
\begin{document}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    34
105
80218dddbb15 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 95
diff changeset
    35
\title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions (Proof Pearl)}
95
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    36
\author{Fahad Ausaf\inst{1} \and Roy Dyckhoff\inst{2} \and Christian Urban\inst{1}}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    37
\institute{King's College London, United Kingdom \and 
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    38
           St Andrews}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    39
\maketitle
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    40
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    41
\begin{abstract}
105
80218dddbb15 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 95
diff changeset
    42
\Brz{} introduced the notion of derivatives of regular expressions
80218dddbb15 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 95
diff changeset
    43
that can be used for very simple regular expression matching algorithms.
80218dddbb15 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 95
diff changeset
    44
95
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    45
BLA BLA  Sulzmann and Lu \cite{Sulzmann2014}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    46
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    47
{\bf Keywords:} 
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    48
\end{abstract}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    49
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    50
\input{session}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    51
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    52
\end{document}
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    53
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    54
%%% Local Variables:
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    55
%%% mode: latex
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    56
%%% TeX-master: t
a33d3040bf7e started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    57
%%% End: