--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Paper/document/lipics-v2021.cls Tue Jan 25 13:12:50 2022 +0000
@@ -0,0 +1,1249 @@
+%%
+%% This is file `lipics-v2021.cls'.
+%%
+%% -----------------------------------------------------------------
+%% Author: Dagstuhl Publishing & le-tex publishing services
+%%
+%% This file is part of the lipics package for preparing
+%% LIPICS articles.
+%%
+%% Copyright (C) 2021 Schloss Dagstuhl
+%%
+%% This work may be distributed and/or modified under the
+%% conditions of the LaTeX Project Public License, either version 1.3
+%% of this license or (at your option) any later version.
+%% The latest version of this license is in
+%% http://www.latex-project.org/lppl.txt
+%% and version 1.3 or later is part of all distributions of LaTeX
+%% version 2005/12/01 or later.
+%%
+%% This work has the LPPL maintenance status `maintained'.
+%%
+%% The Current Maintainer of this work is
+%% Schloss Dagstuhl (publishing@dagstuhl.de).
+%% -----------------------------------------------------------------
+%%
+\ProvidesClass{lipics-v2021}
+ [2021/05/04 v3.1.2 LIPIcs articles]
+\NeedsTeXFormat{LaTeX2e}[2015/01/01]
+\emergencystretch1em
+\advance\hoffset-1in
+\advance\voffset-1in
+\advance\hoffset2.95mm
+\newif\if@nobotseplist \@nobotseplistfalse
+\def\@endparenv{%
+ \addpenalty\@endparpenalty\if@nobotseplist\else\addvspace\@topsepadd\fi\@endpetrue}
+\def\@doendpe{%
+ \@endpetrue
+ \def\par{\@restorepar
+ \everypar{}%
+ \par
+ \if@nobotseplist
+ \addvspace\topsep
+ \addvspace\partopsep
+ \global\@nobotseplistfalse
+ \fi
+ \@endpefalse}%
+ \everypar{{\setbox\z@\lastbox}%
+ \everypar{}%
+ \if@nobotseplist\global\@nobotseplistfalse\fi
+ \@endpefalse}}
+\def\enumerate{%
+ \ifnum \@enumdepth >\thr@@\@toodeep\else
+ \advance\@enumdepth\@ne
+ \edef\@enumctr{enum\romannumeral\the\@enumdepth}%
+ \expandafter
+ \list
+ \csname label\@enumctr\endcsname
+ {\advance\partopsep\topsep
+ \topsep\z@\@plus\p@
+ \ifnum\@listdepth=\@ne
+ \labelsep0.72em
+ \else
+ \ifnum\@listdepth=\tw@
+ \labelsep0.3em
+ \else
+ \labelsep0.5em
+ \fi
+ \fi
+ \usecounter\@enumctr\def\makelabel##1{\hss\llap{##1}}}%
+ \fi}
+\def\endenumerate{\ifnum\@listdepth=\@ne\global\@nobotseplisttrue\fi\endlist}
+\def\itemize{%
+ \ifnum \@itemdepth >\thr@@\@toodeep\else
+ \advance\@itemdepth\@ne
+ \edef\@itemitem{labelitem\romannumeral\the\@itemdepth}%
+ \expandafter
+ \list
+ \csname\@itemitem\endcsname
+ {\advance\partopsep\topsep
+ \topsep\z@\@plus\p@
+ \ifnum\@listdepth=\@ne
+ \labelsep0.83em
+ \else
+ \ifnum\@listdepth=\tw@
+ \labelsep0.75em
+ \else
+ \labelsep0.5em
+ \fi
+ \fi
+ \def\makelabel##1{\hss\llap{##1}}}%
+ \fi}
+\def\enditemize{\ifnum\@listdepth=\@ne\global\@nobotseplisttrue\fi\endlist}
+\def\@title{\textcolor{red}{Author: Please provide a title}}
+\let\@subtitle\@empty
+\def\subtitle#1{\gdef\@subtitle{#1}}
+\def\subtitleseperator{: }
+\def\@sect#1#2#3#4#5#6[#7]#8{%
+ \ifnum #2>\c@secnumdepth
+ \let\@svsec\@empty
+ \else
+ \refstepcounter{#1}%
+ \protected@edef\@svsec{\@seccntformat{#1}\relax}%
+ \fi
+ \@tempskipa #5\relax
+ \ifdim \@tempskipa>\z@
+ \begingroup
+ #6{%
+ \@hangfrom{\hskip #3\relax
+ \ifnum #2=1
+ \colorbox{lipicsYellow}{\kern0.15em\@svsec\kern0.15em}\quad
+ \else
+ \@svsec\quad
+ \fi}%
+ \interlinepenalty \@M #8\@@par}%
+ \endgroup
+ \csname #1mark\endcsname{#7}%
+ \addcontentsline{toc}{#1}{%
+ \ifnum #2>\c@secnumdepth \else
+ \protect\numberline{\csname the#1\endcsname}%
+ \fi
+ #7}%
+ \else
+ \def\@svsechd{%
+ #6{\hskip #3\relax
+ \@svsec #8}%
+ \csname #1mark\endcsname{#7}%
+ \addcontentsline{toc}{#1}{%
+ \ifnum #2>\c@secnumdepth \else
+ \protect\numberline{\csname the#1\endcsname}%
+ \fi
+ #7}}%
+ \fi
+ \@xsect{#5}}
+\def\@seccntformat#1{\csname the#1\endcsname}
+\def\@biblabel#1{\textcolor{lipicsGray}{\sffamily\bfseries#1}}
+\def\EventLogoHeight{25}
+\def\copyrightline{%
+ \ifx\@hideLIPIcs\@undefined
+ \ifx\@EventLogo\@empty
+ \else
+ \setbox\@tempboxa\hbox{\includegraphics[height=\EventLogoHeight\p@]{\@EventLogo}}%
+ \rlap{\hspace\textwidth\hspace{-\wd\@tempboxa}\hspace{\z@}%
+ \vtop to\z@{\vskip-0mm\unhbox\@tempboxa\vss}}%
+ \fi
+ \scriptsize
+ \vtop{\hsize\textwidth
+ \nobreakspace\par
+ \@Copyright
+ \ifx\@EventLongTitle\@empty\else\@EventLongTitle.\\\fi
+ \ifx\@EventEditors\@empty\else
+ \@Eds: \@EventEditors
+ ; Article~No.\,\@ArticleNo; pp.\,\@ArticleNo:\thepage--\@ArticleNo:\number\numexpr\getpagerefnumber{TotPages}%
+ \\
+ \fi
+ \setbox\@tempboxa\hbox{\IfFileExists{lipics-logo-bw.pdf}{\includegraphics[height=14\p@,trim=0 15 0 0]{lipics-logo-bw}}{\includegraphics[height=14\p@, width=62pt]{example-image-plain}}}%
+ \hspace*{\wd\@tempboxa}\enskip
+ \href{https://www.dagstuhl.de/lipics/}%
+ {Leibniz International Proceedings in Informatics}\\
+ \smash{\unhbox\@tempboxa}\enskip
+ \href{https://www.dagstuhl.de}%
+ {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik, Dagstuhl Publishing, Germany}}%
+ \fi}
+\def\ps@plain{\let\@mkboth\@gobbletwo
+ \let\@oddhead\@empty
+ \let\@evenhead\@empty
+ \let\@evenfoot\copyrightline
+ \let\@oddfoot\copyrightline}
+\def\lipics@opterrshort{Option "\CurrentOption" not supported}
+\def\lipics@opterrlong{The option "\CurrentOption" from article.cls is not supported by lipics.cls.}
+\DeclareOption{a5paper}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}}
+\DeclareOption{b5paper}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}}
+\DeclareOption{legalpaper}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}}
+\DeclareOption{executivepaper}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}}
+\DeclareOption{landscape}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}}
+\DeclareOption{10pt}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}}
+\DeclareOption{11pt}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}}
+\DeclareOption{12pt}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}}
+\DeclareOption{oneside}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}}
+\DeclareOption{twoside}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}}
+\DeclareOption{titlepage}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}}
+\DeclareOption{notitlepage}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}}
+\DeclareOption{onecolumn}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}}
+\DeclareOption{twocolumn}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}}
+\DeclareOption{fleqn}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}}
+\DeclareOption{openbib}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}}
+\DeclareOption{a4paper}{\PassOptionsToClass{\CurrentOption}{article}
+ \advance\hoffset-2.95mm
+ \advance\voffset8.8mm}
+\DeclareOption{numberwithinsect}{\let\numberwithinsect\relax}
+\DeclareOption{cleveref}{\let\usecleveref\relax}
+\DeclareOption{autoref}{\let\useautoref\relax}
+\DeclareOption{anonymous}{\let\authoranonymous\relax}
+\DeclareOption{thm-restate}{\let\usethmrestate\relax}
+\DeclareOption{authorcolumns}{\let\authorcolumns\relax}
+\let\compactauthor\relax
+\DeclareOption{oldauthorstyle}{\let\compactauthor\@empty}
+\DeclareOption{compactauthor}{\let\compactauthor\relax}
+\DeclareOption{pdfa}{\let\pdfa\relax}
+\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}}
+\ProcessOptions
+\LoadClass[twoside,notitlepage,fleqn]{article}
+\renewcommand\normalsize{%
+ \@setfontsize\normalsize\@xpt{13}%
+ \abovedisplayskip 10\p@ \@plus2\p@ \@minus5\p@
+ \abovedisplayshortskip \z@ \@plus3\p@
+ \belowdisplayshortskip 6\p@ \@plus3\p@ \@minus3\p@
+ \belowdisplayskip \abovedisplayskip
+ \let\@listi\@listI}
+\normalsize
+\renewcommand\small{%
+ \@setfontsize\small\@ixpt{11.5}%
+ \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@
+ \abovedisplayshortskip \z@ \@plus2\p@
+ \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@
+ \def\@listi{\leftmargin\leftmargini
+ \topsep 4\p@ \@plus2\p@ \@minus2\p@
+ \parsep 2\p@ \@plus\p@ \@minus\p@
+ \itemsep \parsep}%
+ \belowdisplayskip \abovedisplayskip
+}
+\renewcommand\footnotesize{%
+ \@setfontsize\footnotesize{8.5}{9.5}%
+ \abovedisplayskip 6\p@ \@plus2\p@ \@minus4\p@
+ \abovedisplayshortskip \z@ \@plus\p@
+ \belowdisplayshortskip 3\p@ \@plus\p@ \@minus2\p@
+ \def\@listi{\leftmargin\leftmargini
+ \topsep 3\p@ \@plus\p@ \@minus\p@
+ \parsep 2\p@ \@plus\p@ \@minus\p@
+ \itemsep \parsep}%
+ \belowdisplayskip \abovedisplayskip
+}
+\renewcommand\large{\@setfontsize\large{10.5}{13}}
+\renewcommand\Large{\@setfontsize\Large{12}{14}}
+\setlength\parindent{1.5em}
+\setlength\headheight{3mm}
+\setlength\headsep {10mm}
+\setlength\footskip{3mm}
+\setlength\textwidth{140mm}
+\setlength\textheight{222mm}
+\setlength\oddsidemargin{32mm}
+\setlength\evensidemargin{38mm}
+\setlength\marginparwidth{25mm}
+\setlength\topmargin{13mm}
+\setlength{\skip\footins}{2\baselineskip \@plus 4\p@ \@minus 2\p@}
+\def\@listi{\leftmargin\leftmargini
+ \parsep\z@ \@plus\p@
+ \topsep 8\p@ \@plus2\p@ \@minus4\p@
+ \itemsep \parsep}
+\let\@listI\@listi
+\@listi
+\def\@listii {\leftmargin\leftmarginii
+ \labelwidth\leftmarginii
+ \advance\labelwidth-\labelsep
+ \topsep 4\p@ \@plus2\p@ \@minus\p@
+ \parsep\z@ \@plus\p@
+ \itemsep \parsep}
+\def\@listiii{\leftmargin\leftmarginiii
+ \labelwidth\leftmarginiii
+ \advance\labelwidth-\labelsep
+ \topsep 2\p@ \@plus\p@\@minus\p@
+ \parsep \z@
+ \partopsep \p@ \@plus\z@ \@minus\p@
+ \itemsep \z@ \@plus\p@}
+\def\ps@headings{%
+ \def\@evenhead{\large\sffamily\bfseries
+ \llap{\hbox to0.5\oddsidemargin{ \ifx\@hideLIPIcs\@undefined\ifx\@ArticleNo\@empty\textcolor{red}{XX}\else\@ArticleNo\fi:\fi\thepage\hss}}\leftmark\hfil}%
+ \def\@oddhead{\large\sffamily\bfseries\rightmark\hfil
+ \rlap{\hbox to0.5\oddsidemargin{\hss \ifx\@hideLIPIcs\@undefined\ifx\@ArticleNo\@empty\textcolor{red}{XX}\else\@ArticleNo\fi:\fi\thepage}}}%
+ \def\@oddfoot{\hfil
+ \rlap{%
+ \vtop{%
+ \vskip10mm
+ \colorbox{lipicsYellow}
+ {\@tempdima\evensidemargin
+ \advance\@tempdima1in
+ \advance\@tempdima\hoffset
+ \hb@xt@\@tempdima{%
+ \ifx\@hideLIPIcs\@undefined
+ \textcolor{lipicsGray}{\normalsize\sffamily
+ \bfseries\quad
+ \expandafter\textsolittle
+ \expandafter{\@EventShortTitle}}%
+ \fi
+ \strut\hss}}}}}
+ \let\@evenfoot\@empty
+ \let\@mkboth\markboth
+ \let\sectionmark\@gobble
+ \let\subsectionmark\@gobble}
+\pagestyle{headings}
+\renewcommand\maketitle{\par
+ \begingroup
+ \thispagestyle{plain}
+ \renewcommand\thefootnote{\@fnsymbol\c@footnote}%
+ \if@twocolumn
+ \ifnum \col@number=\@ne
+ \@maketitle
+ \else
+ \twocolumn[\@maketitle]%
+ \fi
+ \else
+ \newpage
+ \global\@topnum\z@ % Prevents figures from going at top of page.
+ \@maketitle
+ \fi
+ \thispagestyle{plain}\@thanks
+ \endgroup
+ \global\let\thanks\relax
+ \global\let\maketitle\relax
+ \global\let\@maketitle\relax
+ \global\let\@thanks\@empty
+ \global\let\@author\@empty
+ \global\let\@date\@empty
+ \global\let\@title\@empty
+ \global\let\@subtitle\@empty
+ \global\let\title\relax
+ \global\let\author\relax
+ \global\let\date\relax
+ \global\let\and\relax
+}
+\newwrite\tocfile
+\def\@maketitle{%
+ \newpage
+ \null\vskip-\baselineskip
+ \vskip-\headsep
+ \@titlerunning
+ \@authorrunning
+ %%\let \footnote \thanks
+ \parindent\z@ \raggedright
+ \if!\@title!\def\@title{\textcolor{red}{Author: Please fill in a title}}\fi
+ {\LARGE\sffamily\bfseries\mathversion{bold}\@title \if!\@subtitle!\else{\\\Large\sffamily\bfseries\mathversion{bold}\@subtitle}\fi \par}%
+ \vskip 1em
+ \ifx\@author\orig@author
+ \textcolor{red}{Author: Please provide author information}%
+ \else
+ {\def\thefootnote{\@arabic\c@footnote}%
+ \setcounter{footnote}{0}%
+ \fontsize{9.5}{12}\selectfont\@author}%
+ \fi
+ \bgroup
+ \immediate\openout\tocfile=\jobname.vtc
+ \protected@write\tocfile{
+ \let\footnote\@gobble
+ \let\thanks\@gobble
+ \def\footnotemark{}
+ \def\and{and }%
+ \def\,{ }
+ \def\\{ }
+ }{%
+ \string\contitem
+ \string\title{\@title \if!\@subtitle!\else\subtitleseperator \@subtitle\fi}%
+ \string\author{\@authorsfortoc}%
+ \string\page{\@ArticleNo:\thepage--\@ArticleNo:\number\numexpr\getpagerefnumber{TotPages}}}%
+ \closeout\tocfile
+ \egroup
+ \par}
+\renewcommand\tableofcontents{%
+ \section*{\contentsname}%
+ \@starttoc{toc}}
+\setcounter{secnumdepth}{4}
+\renewcommand\section{\@startsection {section}{1}{\z@}%
+ {-3.5ex \@plus -1ex \@minus -.2ex}%
+ {2.3ex \@plus.2ex}%
+ {\sffamily\Large\bfseries\raggedright}}
+\renewcommand\subsection{\@startsection{subsection}{2}{\z@}%
+ {-3.25ex\@plus -1ex \@minus -.2ex}%
+ {1.5ex \@plus .2ex}%
+ {\sffamily\Large\bfseries\raggedright}}
+\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}%
+ {-3.25ex\@plus -1ex \@minus -.2ex}%
+ {1.5ex \@plus .2ex}%
+ {\sffamily\Large\bfseries\raggedright}}
+\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
+ {-3.25ex \@plus-1ex \@minus-.2ex}%
+ {1.5ex \@plus .2ex}%
+ {\sffamily\large\bfseries\raggedright}}
+\renewcommand\subparagraph{\@startsection{subparagraph}{5}{\z@}%
+ {3.25ex \@plus1ex \@minus .2ex}%
+ {-1em}%
+ {\sffamily\normalsize\bfseries}}
+\newcommand{\proofsubparagraph}{\@startsection{subparagraph}{5}{\z@}%
+ {3.25ex \@plus1ex \@minus .2ex}%
+ {-1em}%
+ {\color{lipicsGray}\sffamily\normalsize\bfseries}}
+\setlength\leftmargini \parindent
+\setlength\leftmarginii {1.2em}
+\setlength\leftmarginiii{1.2em}
+\setlength\leftmarginiv {1.2em}
+\setlength\leftmarginv {1.2em}
+\setlength\leftmarginvi {1.2em}
+\renewcommand\labelenumi{%
+ \textcolor{lipicsGray}{\sffamily\bfseries\upshape\mathversion{bold}\theenumi.}}
+\renewcommand\labelenumii{%
+ \textcolor{lipicsGray}{\sffamily\bfseries\upshape\mathversion{bold}\theenumii.}}
+\renewcommand\labelenumiii{%
+ \textcolor{lipicsGray}{\sffamily\bfseries\upshape\mathversion{bold}\theenumiii.}}
+\renewcommand\labelenumiv{%
+ \textcolor{lipicsGray}{\sffamily\bfseries\upshape\mathversion{bold}\theenumiv.}}
+\renewcommand\labelitemi{%
+ \textcolor{lipicsBulletGray}{\ifnum\@listdepth=\@ne
+ \rule{0.67em}{0.33em}%
+ \else
+ \rule{0.45em}{0.225em}%
+ \fi}}
+\renewcommand\labelitemii{%
+ \textcolor{lipicsBulletGray}{\rule{0.45em}{0.225em}}}
+\renewcommand\labelitemiii{%
+ \textcolor{lipicsBulletGray}{\sffamily\bfseries\textasteriskcentered}}
+\renewcommand\labelitemiv{%
+ \textcolor{lipicsBulletGray}{\sffamily\bfseries\textperiodcentered}}
+\renewenvironment{description}
+ {\list{}{\advance\partopsep\topsep\topsep\z@\@plus\p@
+ \labelwidth\z@ \itemindent-\leftmargin
+ \let\makelabel\descriptionlabel}}
+ {\ifnum\@listdepth=\@ne\global\@nobotseplisttrue\fi\endlist}
+\renewcommand*\descriptionlabel[1]{%
+ \hspace\labelsep\textcolor{lipicsGray}{\sffamily\bfseries\mathversion{bold}#1}}
+\def\topmattervskip{0.7}
+\renewenvironment{abstract}{%
+ \vskip\topmattervskip\bigskipamount
+ \noindent
+ \rlap{\color{lipicsLineGray}\vrule\@width\textwidth\@height1\p@}%
+ \hspace*{7mm}\fboxsep1.5mm\colorbox[rgb]{1,1,1}{\raisebox{-0.4ex}{%
+ \large\selectfont\sffamily\bfseries\abstractname}}%
+ \vskip3\p@
+ \fontsize{9}{12}\selectfont
+ \noindent\ignorespaces}
+ {\vskip\topmattervskip\baselineskip\noindent
+ \subjclassHeading
+ \ifx\@ccsdescString\@empty
+ \textcolor{red}{Author: Please fill in 1 or more \string\ccsdesc\space macro}%
+ \else
+ \@ccsdescString
+ \fi
+ \vskip\topmattervskip\baselineskip
+ \noindent\keywordsHeading
+ \ifx\@keywords\@empty
+ \textcolor{red}{Author: Please fill in \string\keywords\space macro}%
+ \else
+ \@keywords
+ \fi
+ \ifx\@hideLIPIcs\@undefined
+ \ifx\@DOIPrefix\@empty\else
+ \vskip\topmattervskip\baselineskip\noindent
+ \doiHeading\href{https://doi.org/\@lipicsdoi}{\@lipicsdoi}%
+ \fi
+ \fi
+ \ifx\@category\@empty\else
+ \vskip\topmattervskip\baselineskip\noindent
+ \categoryHeading\@category
+ \fi
+ \ifx\@relatedversion\@empty\else
+ \vskip\topmattervskip\baselineskip\noindent
+ \relatedversionHeading\ifx\authoranonymous\relax\textcolor{red}{Anonymous related version(s)}\else\@relatedversion\fi
+ \fi
+ \ifx\@supplement\@empty\else
+ \vskip\topmattervskip\baselineskip\noindent
+ \supplementHeading\ifx\authoranonymous\relax\textcolor{red}{Anonymous supplementary material}\else\@supplement\fi
+ \fi
+ \ifx\@funding\@empty\else
+ \vskip\topmattervskip\baselineskip\noindent
+ \fundingHeading\ifx\authoranonymous\relax\textcolor{red}{Anonymous funding}\else\@funding\fi
+ \fi
+ \ifx\@acknowledgements\@empty\else
+ \vskip\topmattervskip\baselineskip\noindent
+ \acknowledgementsHeading\ifx\authoranonymous\relax\textcolor{red}{Anonymous acknowledgements} \else\@acknowledgements\fi
+ \fi
+ \protected@write\@auxout{}{\string\gdef\string\@pageNumberEndAbstract{\thepage}}%
+ }% end abstract
+\renewenvironment{thebibliography}[1]
+ {\if@noskipsec \leavevmode \fi
+ \par
+ \@tempskipa-3.5ex \@plus -1ex \@minus -.2ex\relax
+ \@afterindenttrue
+ \@tempskipa -\@tempskipa \@afterindentfalse
+ \if@nobreak
+ \everypar{}%
+ \else
+ \addpenalty\@secpenalty\addvspace\@tempskipa
+ \fi
+ \noindent
+ \rlap{\color{lipicsLineGray}\vrule\@width\textwidth\@height1\p@}%
+ \hspace*{7mm}\fboxsep1.5mm\colorbox[rgb]{1,1,1}{\raisebox{-0.4ex}{%
+ \normalsize\sffamily\bfseries\refname}}%
+ \@xsect{1ex \@plus.2ex}%
+ \list{\@biblabel{\@arabic\c@enumiv}}%
+ {\leftmargin8.5mm
+ \labelsep\leftmargin
+ \settowidth\labelwidth{\@biblabel{#1}}%
+ \advance\labelsep-\labelwidth
+ \usecounter{enumiv}%
+ \let\p@enumiv\@empty
+ \renewcommand\theenumiv{\@arabic\c@enumiv}}%
+ \fontsize{9}{12}\selectfont
+ \sloppy
+ \clubpenalty4000
+ \@clubpenalty \clubpenalty
+ \widowpenalty4000%
+ \sfcode`\.\@m\protected@write\@auxout{}{\string\gdef\string\@pageNumberStartBibliography{\thepage}}}
+ {\def\@noitemerr
+ {\@latex@warning{Empty `thebibliography' environment}}%
+ \protected@write\@auxout{}{\string\gdef\string\@pageNumberEndBibliography{\thepage}}%
+ \endlist}
+\g@addto@macro\appendix{\immediate\write\@auxout{\string\gdef\string\@pageNumberStartAppendix{\thepage}}}%
+\renewcommand\footnoterule{%
+ \kern-8\p@
+ {\color{lipicsBulletGray}\hrule\@width40mm\@height1\p@}%
+ \kern6.6\p@}
+\renewcommand\@makefntext[1]{%
+ \parindent\z@\hangindent1em
+ \leavevmode
+ \hb@xt@1em{\@makefnmark\hss}#1}
+\usepackage{microtype}
+\usepackage[utf8]{inputenc}
+\ifx\pdfa\relax%
+ \IfFileExists{glyphtounicode.tex}{
+ \input glyphtounicode
+ \pdfgentounicode=1
+ }{}%
+\fi
+\IfFileExists{lmodern.sty}{\RequirePackage{lmodern}}{}
+\IfFileExists{fontawesome5.sty}{%
+\RequirePackage{fontawesome5}%
+\IfFileExists{orcid.pdf}{%
+\def\orcidsymbol{\includegraphics[height=9\p@]{orcid}}
+}{
+\def\orcidsymbol{\textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries \faOrcid}}%
+}
+\def\mailsymbol{\textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries \faIcon[regular]{envelope}}}%
+\def\homesymbol{\textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries \faHome}}%
+}{%
+\ClassWarning{Package fontawesome5 not installed}{Please install package fontawesome5}
+\def\orcidsymbol{\textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries ORCID}}
+\def\mailsymbol{\textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries @}}%
+\def\homesymbol{\textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries H}}%
+}%
+\RequirePackage[T1]{fontenc}
+\RequirePackage{textcomp}
+\RequirePackage[mathscr]{eucal}
+\RequirePackage{amssymb}
+\PassOptionsToPackage{retainmissing}{MnSymbol}
+\AtBeginDocument{\@ifpackageloaded{MnSymbol}%
+ {\expandafter\let\csname ver@amssymb.sty\endcsname\relax
+ \let\complement\@undefined
+ \RequirePackage{amssymb}}{}}
+\RequirePackage{soul}
+\sodef\textsolittle{}{.12em}{.5em\@plus.08em\@minus.06em}%
+ {.4em\@plus.275em\@minus.183em}
+\RequirePackage{color} %kept for backward compatibility
+\AtBeginDocument{
+ \@ifpackageloaded{xcolor}{
+ }{
+ \RequirePackage{xcolor}
+ }
+ \definecolor{darkgray}{rgb}{0.31,0.31,0.33}
+ \definecolor[named]{lipicsGray}{rgb}{0.31,0.31,0.33}
+ \definecolor[named]{lipicsBulletGray}{rgb}{0.60,0.60,0.61}
+ \definecolor[named]{lipicsLineGray}{rgb}{0.51,0.50,0.52}
+ \definecolor[named]{lipicsLightGray}{rgb}{0.85,0.85,0.86}
+ \definecolor[named]{lipicsYellow}{rgb}{0.99,0.78,0.07}
+}
+\RequirePackage{babel}
+\RequirePackage[tbtags,fleqn]{amsmath}
+\AtBeginDocument{
+ \@ifpackageloaded{enumitem}{\ClassWarning{Package 'enumitem' incompatible}{Don't use package 'enumitem'; Package enumerate preloaded!}}{}
+ \@ifpackageloaded{paralist}{\ClassWarning{Package 'paralist' incompatible}{Don't use package 'paralist'; Package enumerate preloaded!}}{}
+}
+\RequirePackage{enumerate}
+\def\@enum@{\list{\textcolor{lipicsGray}{\sffamily\bfseries\upshape\mathversion{bold}\csname label\@enumctr\endcsname}}%
+ {\advance\partopsep\topsep
+ \topsep\z@\@plus\p@
+ \usecounter{\@enumctr}\def\makelabel##1{\hss\llap{##1}}}}
+\def\romanenumerate{\enumerate[(i)]}
+\let\endromanenumerate\endenumerate
+\def\alphaenumerate{\enumerate[(a)]}
+\let\endalphaenumerate\endenumerate
+\def\bracketenumerate{\enumerate[(1)]}
+\let\endbracketenumerate\endenumerate
+\RequirePackage{graphicx}
+\RequirePackage{array}
+\let\@classzold\@classz
+\def\@classz{%
+ \expandafter\ifx\d@llarbegin\begingroup
+ \toks \count@ =
+ \expandafter{\expandafter\small\the\toks\count@}%
+ \fi
+ \@classzold}
+\RequirePackage{multirow}
+\RequirePackage{tabularx}
+\RequirePackage[online]{threeparttable}
+\def\TPTtagStyle#1{#1)}
+\def\tablenotes{\small\TPT@defaults
+ \@ifnextchar[\TPT@setuptnotes\TPTdoTablenotes} % ]
+\RequirePackage{listings}
+\lstset{basicstyle=\small\ttfamily,%
+ backgroundcolor=\color{lipicsLightGray},%
+ frame=single,framerule=0pt,xleftmargin=\fboxsep,xrightmargin=\fboxsep}
+\RequirePackage[left,mathlines]{lineno}
+\linenumbers
+\renewcommand\linenumberfont{\normalfont\tiny\sffamily}
+%%%% patch to cope with amsmath
+%%%% http://phaseportrait.blogspot.de/2007/08/lineno-and-amsmath-compatibility.html
+\newcommand*\patchAmsMathEnvironmentForLineno[1]{%
+ \expandafter\let\csname old#1\expandafter\endcsname\csname #1\endcsname
+ \expandafter\let\csname oldend#1\expandafter\endcsname\csname end#1\endcsname
+ \renewenvironment{#1}%
+ {\linenomath\csname old#1\endcsname}%
+ {\csname oldend#1\endcsname\endlinenomath}}%
+\newcommand*\patchBothAmsMathEnvironmentsForLineno[1]{%
+ \patchAmsMathEnvironmentForLineno{#1}%
+ \patchAmsMathEnvironmentForLineno{#1*}}%
+\AtBeginDocument{%
+ \patchBothAmsMathEnvironmentsForLineno{equation}%
+ \patchBothAmsMathEnvironmentsForLineno{align}%
+ \patchBothAmsMathEnvironmentsForLineno{flalign}%
+ \patchBothAmsMathEnvironmentsForLineno{alignat}%
+ \patchBothAmsMathEnvironmentsForLineno{gather}%
+ \patchBothAmsMathEnvironmentsForLineno{multline}}
+\let\usehyperxmp\@empty%
+\ifx\pdfa\relax%
+ \IfFileExists{hyperxmp.sty}{%
+ \RequirePackage{hyperxmp}%
+ \@ifpackagelater{hyperxmp}{2019/04/05}{%
+ \let\usehyperxmp\relax%
+ }{%
+ \ClassWarning{Package hyperxmp outdated}{You are using an outdated version of the package hyperxmp. Please update!}%
+ }}{}%
+\fi%
+\IfFileExists{totpages.sty}{
+ \RequirePackage{totpages}
+}{
+ \ClassWarning{Package totpages not installed}{Please install package totpages}
+ \newcounter{TotPages}
+ \setcounter{TotPages}{99}
+}
+\ifx\usehyperxmp\relax%
+ \RequirePackage[pdfa,unicode]{hyperref}%
+\else%
+ \RequirePackage[unicode]{hyperref}%
+\fi%
+\let\C\relax%
+\let\G\relax%
+\let\F\relax%
+\let\U\relax%
+\pdfstringdefDisableCommands{%
+ \let\thanks\@gobble%
+ \let\footnote\@gobble%
+ \def\footnotemark{}%
+ \def\cs#1{\textbackslash #1}%
+ \let\normalfont\@empty%
+ \let\scshape\@empty%
+ \def\and{and }%
+ \def\,{ }%
+ \def\textrightarrow{ -> }%
+ \let\mathsf\@empty%
+}%
+\hypersetup{
+ breaklinks=true,
+ pdfencoding=unicode,
+ bookmarksnumbered,
+ pdfborder={0 0 0},
+ pdfauthor={ }
+}%
+\AtBeginDocument{
+\ifx\usehyperxmp\relax
+\hypersetup{
+pdftitle={\@title \if!\@subtitle!\else\subtitleseperator \@subtitle\fi},
+pdfauthor={\ifx\authoranonymous\relax Anonymous author(s) \else \@authorsforpdf \fi},
+pdfkeywords={\@keywords},
+pdfproducer={LaTeX with lipics-v2021.cls},
+pdfsubject={LIPIcs, Vol.\@SeriesVolume, \@EventShortTitle},
+pdfcopyright = { Copyright (C) \ifx\authoranonymous\relax Anonymous author(s) \else \@copyrightholder; \fi licensed under Creative Commons License CC-BY 4.0},
+pdflang={en},
+pdfmetalang={en},
+pdfpublisher={Schloss Dagstuhl -- Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany},
+pdflicenseurl={https://creativecommons.org/licenses/by/4.0/},
+pdfpubtype={LIPIcs},
+pdfvolumenum={\@SeriesVolume},
+pdfpagerange={\@ArticleNo:\thepage-\@ArticleNo:\theTotPages},
+pdfdoi={\@lipicsdoi},
+pdfapart=3,
+pdfaconformance=B
+}
+\else%
+\hypersetup{
+pdftitle={\@title \if!\@subtitle!\else\subtitleseperator \@subtitle\fi},
+pdfauthor={\ifx\authoranonymous\relax Anonymous author(s) \else \@authorsforpdf \fi},
+pdfkeywords={\@keywords},
+pdfcreator={LaTeX with lipics-v2021.cls},
+pdfsubject={LIPIcs, Vol.\@SeriesVolume, \@EventShortTitle; Copyright (C) \ifx\authoranonymous\relax Anonymous author(s) \else \@copyrightholder; \fi licensed under Creative Commons License CC-BY 4.0}
+}%
+\fi %
+}
+\ifx\usehyperxmp\relax
+\pdfobjcompresslevel=0
+\pdfinclusioncopyfonts=1
+\IfFileExists{colorprofiles.tex}{
+\RequirePackage{colorprofiles}%
+\IfFileExists{sRGB.icc}{
+\immediate\pdfobj stream attr{/N 3} file{sRGB.icc}
+\pdfcatalog{%
+/OutputIntents [
+<<
+/Type /OutputIntent
+/S /GTS_PDFA1
+/DestOutputProfile \the\pdflastobj\space 0 R
+/OutputConditionIdentifier (sRGB)
+/Info (sRGB)
+>>
+]
+}}{}
+}{\ClassWarning{Package colorprofiles not installed}{Please install package colorprofiles}}
+\fi
+\RequirePackage[labelsep=space,singlelinecheck=false,%
+ font={up,small},labelfont={sf,bf},%
+ listof=false]{caption}%"listof" instead of "list" for backward compatibility
+\@ifpackagelater{hyperref}{2009/12/09}
+ {\captionsetup{compatibility=false}}%cf. http://groups.google.de/group/comp.text.tex/browse_thread/thread/db9310eb540fbbd8/42e30f3b7b3aa17a?lnk=raot
+ {}
+\DeclareCaptionLabelFormat{boxed}{%
+ \kern0.05em{\color[rgb]{0.99,0.78,0.07}\rule{0.73em}{0.73em}}%
+ \hspace*{0.67em}\bothIfFirst{#1}{~}#2}
+\captionsetup{labelformat=boxed}
+\captionsetup[table]{position=top}
+\RequirePackage[figuresright]{rotating}
+\caption@AtBeginDocument{\@ifpackageloaded{subfig}{\ClassError{lipics}{%
+ Do not load the subfig package}{The more recent subcaption package is already loaded}}{}}
+\RequirePackage{subcaption}
+\def\titlerunning#1{\gdef\@titlerunning{{\let\footnote\@gobble\markboth{#1}{#1}}}}
+\def\authorrunning#1{%
+ \gdef\@authorrunning{\markright{\ifx\authoranonymous\relax\textcolor{red}{Anonymous author(s)} \else\if!#1!\textcolor{red}{Author: Please fill in the \string\authorrunning\space macro}\else#1\fi\fi}}}
+\titlerunning{\@title \if!\@subtitle!\else\subtitleseperator \@subtitle\fi}
+\authorrunning{\textcolor{red}{Author: Please use the \string\authorrunning\space macro}}
+\def\EventLongTitle#1{\gdef\@EventLongTitle{#1}}
+\EventLongTitle{}
+\def\EventShortTitle#1{\gdef\@EventShortTitle{#1}}
+\EventShortTitle{}
+\def\EventEditors#1{\gdef\@EventEditors{#1}}
+\EventEditors{}
+\def\EventNoEds#1{\gdef\@EventNoEds{#1}\xdef\@Eds{Editor\ifnum#1>1s\fi}}
+\EventNoEds{1}
+\def\EventLogo#1{\gdef\@EventLogo{#1}}
+\EventLogo{}
+\def\EventAcronym#1{\gdef\@EventAcronym{#1}}
+\EventAcronym{}
+\def\EventYear#1{\gdef\@EventYear{#1}}
+\EventYear{}
+\def\EventDate#1{\gdef\@EventDate{#1}}
+\EventDate{}
+\def\EventLocation#1{\gdef\@EventLocation{#1}}
+\EventLocation{}
+\def\SeriesVolume#1{\gdef\@SeriesVolume{#1}}
+\SeriesVolume{}
+\def\ArticleNo#1{\gdef\@ArticleNo{#1}}
+\ArticleNo{}
+\def\DOIPrefix#1{\gdef\@DOIPrefix{#1}}
+\DOIPrefix{10.4230/LIPIcs}
+\def\@lipicsdoi{\@DOIPrefix.\@EventAcronym.\@EventYear.\@ArticleNo}
+\def\and{\newline}
+\let\orig@author\@author
+\let\@authorsfortoc\@empty
+\let\@authorsforpdf\@empty
+\newcount\c@author
+\newcounter{currentauthor}
+\def\authorcolumnsMin{6}
+\def\@authornum{0}
+\def\author#1#2#3#4#5{%
+ \ifx\@author\orig@author\let\@author\@empty\fi
+ \g@addto@macro\@author{%
+ \noexpandarg\StrBehind{#2}{\and \url}[\homepageTemp]\IfSubStr{#2}{\and \url}{\StrBefore{#2}{\and \url}[\affiliation]}{\def\affiliation{#2}}%
+ \expandarg\exploregroups\StrRemoveBraces{\homepageTemp}[\homepage]%
+ \ifx\authorcolumns\relax
+ \ifnum\c@author>\authorcolumnsMin
+ \stepcounter{currentauthor}
+ \ifodd\value{currentauthor}
+ \begin{minipage}[t]{\textwidth}
+ \begin{minipage}[t]{0.49\textwidth}
+ \else
+ \hfill \begin{minipage}[t]{0.49\textwidth}
+ \fi
+ \else
+ \ClassWarning{Option 'authorcolumns' only applicable for > 6 authors}{Option 'authorcolumns' only applicable for >6 authors!}
+ \addvspace{0.5\baselineskip}
+ \fi
+ \else
+ \addvspace{0.5\baselineskip}
+ \fi
+ {\Large\bfseries
+ \if!#1!
+ \textcolor{red}{Author: Please enter author name}%
+ \else
+ \ifx\authoranonymous\relax
+ \textcolor{red}{Anonymous author}
+ \else
+ #1\,%
+ \ifx\compactauthor\relax\if!#3!\else{\,\href{mailto:#3}{\mailsymbol}}\fi%
+ \ifx\homepage\@empty\else{\,\href{\homepage}{\homesymbol}}\fi\fi%
+ \if!#4!\else{\,\href{#4}{\orcidsymbol}}\fi%
+ \if!#5!\else
+ \ifx\@funding\@empty
+ \expandafter\g@addto@macro\expandafter\@funding{\textit{\expandafter{\let\footnote\@gobble #1}}:\space{#5}}
+ \else
+ \expandafter\g@addto@macro\expandafter\@funding{\\\textit{\expandafter{\let\footnote\@gobble #1}}:\space{#5}}
+ \fi
+ \fi
+ \fi
+ \fi
+ }
+ {\small
+ \if!#2!\textcolor{red}{Author: Please enter affiliation as second parameter of the author macro}\else{\\* \ifx\authoranonymous\relax\textcolor{red}{Anonymous affiliation}\else\ifx\compactauthor\relax \affiliation \else#2\fi\fi}\fi
+ \ifx\compactauthor\relax\else\if!#3!\else{\ifx\authoranonymous\relax\else\\*\href{mailto:#3}{#3}\fi}\fi\fi
+ }\par
+ \ifx\authorcolumns\relax
+ \ifnum\c@author>\authorcolumnsMin
+ \end{minipage}
+ \ifnum\c@author=\value{currentauthor}
+ \end{minipage}
+ \else
+ \ifodd\value{currentauthor}
+ \else
+ \end{minipage}%
+ \medskip
+ \fi
+ \fi
+ \fi
+ \fi}%
+ \global\advance\c@author\@ne
+ \protected@write\@auxout{}{\string\gdef\string\@authornum{\the\c@author}}
+ \ifnum\c@author=\@ne
+ \gdef\@authorsfortoc{#1}%
+ \gdef\@authorsforpdf{#1}
+ \else
+ \expandafter\g@addto@macro\expandafter\@authorsforpdf\expandafter{, #1}
+ \expandafter\g@addto@macro\expandafter\@authorsfortoc\expandafter{\expandafter\csname\the\c@author authand\endcsname#1}%
+ \@namedef{\the\c@author authand}{,\space}%
+ \AtBeginDocument{%
+ \expandafter\ifnum\@authornum=2
+ \@namedef{2authand}{\space and\space}%
+ \else
+ \@namedef{\@authornum authand}{,\space and\space}%
+ \fi}
+ \fi}
+\newcommand*\affil[2][]{%
+ \ClassError{lipics}
+ {\string\affil\space deprecated: Please enter affiliation as second parameter of the author macro}
+ {Since 2017, \string\affil\space is obsolete in lipics.}}
+\newcommand*\Copyright[1]{%
+ \def\@copyrightholder{#1}
+ \def\@Copyright{%
+ \setbox\@tempboxa\hbox{\IfFileExists{cc-by.pdf}{\includegraphics[height=14\p@,clip]{cc-by}}{\includegraphics[height=14\p@, width=40pt]{example-image-plain}}}%
+ \@rightskip\@flushglue \rightskip\@rightskip
+ \hangindent\dimexpr\wd\@tempboxa+0.5em\relax
+ \href{https://creativecommons.org/licenses/by/4.0/}%
+ {\smash{\lower\baselineskip\hbox{\unhcopy\@tempboxa}}}\enskip
+ \textcopyright\ %
+ \ifx!#1!\textcolor{red}{Author: Please fill in the \string\Copyright\space macro}\else\ifx\authoranonymous\relax\textcolor{red}{Anonymous author(s)}\else#1\fi\fi
+ ;\\%
+ licensed under Creative Commons License CC-BY 4.0\ifx!#1!\\\null\fi\par}}
+\Copyright{\textcolor{red}{Author: Please provide a copyright holder}}
+\let\@copyrightholder\@empty
+\def\hideLIPIcs{\let\@hideLIPIcs\relax}
+\usepackage{xstring}
+\def\keywords#1{\def\@keywords{#1}}
+\let\@keywords\@empty
+\def\keywordsHeading{%
+ \textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries
+ Keywords and phrases\enskip}}
+\RequirePackage{comment}
+\excludecomment{CCSXML}
+% inspired by https://tex.stackexchange.com/questions/12810/how-do-i-split-a-string
+\global\newcommand\ccsdesc[2][100]{\@ccsdesc#1~#2~~\relax}
+\let\orig@ccsdesc\@ccsdesc
+\let\@ccsdesc\@empty
+\let\@ccsdescString\@empty
+\gdef\@ccsdesc#1~#2~#3~{
+ \ifx\@ccsdesc\orig@ccsdesc\let\@ccsdesc\@empty\fi
+ \ifx!#3!
+ \ifx\@ccsdescString\@empty
+ \g@addto@macro\@ccsdescString{{#2}}
+ \else
+ \g@addto@macro\@ccsdescString{; {#2}}
+ \fi
+ \else
+ \ifx\@ccsdescString\@empty
+ \g@addto@macro\@ccsdescString{{#2} $\rightarrow$ {#3}}
+ \else
+ \g@addto@macro\@ccsdescString{; {#2} $\rightarrow$ {#3}}
+ \fi
+ \fi
+\ccsdescEnd
+}
+\def\ccsdescEnd#1\relax{}
+\def\subjclass#1{
+ \ClassError{lipics}
+ {\string\subjclass\space deprecated: Please enter subject classification in 1 or more ccsdesc macros}
+ {Since 2019, \string\subjclass\space is obsolete in lipics.}}
+\let\@subjclass\@empty
+\def\subjclassHeading{%
+ \textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries
+ 2012 ACM Subject Classification\enskip}}
+\def\doiHeading{%
+ \textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries
+ Digital Object Identifier\enskip}}
+\def\category#1{\def\@category{#1}}
+\let\@category\@empty
+\def\categoryHeading{%
+ \textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries
+ Category\enskip}}
+\def\relatedversion#1{\def\@relatedversion{#1}}
+\let\@relatedversion\@empty
+\define@key{relatedversiondetails}{linktext}{\def\relatedversiondetails@linktext{#1}}
+\define@key{relatedversiondetails}{cite}{\def\relatedversiondetails@cite{#1}}
+\newcommand*\addtorelatedversionmacro[2]{%
+ \ifx\@relatedversion\@empty%
+ \g@addto@macro\@relatedversion{#1}%
+ \else%
+ \g@addto@macro\@relatedversion{\\#1}%
+ \fi%
+}%
+\newcommand{\relatedversiondetails}[3][]{%
+ \begingroup%
+ \let\relatedversiondetails@linktext\@empty
+ \let\relatedversiondetails@cite\@empty
+ \setkeys{relatedversiondetails}{#1}%
+ \ifx\relatedversiondetails@linktext\@empty%
+ \protected@edef\tmp{\textit{#2}:\space{\url{#3}}}%
+ \else%
+ \protected@edef\tmp{\textit{#2}:\space{\href{#3}{\texttt{\relatedversiondetails@linktext}}}}%
+ \fi%
+ \ifx\relatedversiondetails@cite\@empty%
+ \else%
+ \protected@edef\tmp{\tmp\nobreakspace\cite{\relatedversiondetails@cite}}%
+ \fi%
+ \expandafter\addtorelatedversionmacro\expandafter{\tmp}{#1}%
+ \endgroup%
+}%
+\def\relatedversionHeading{%
+ \textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries
+ Related Version\enskip}}
+\def\supplement#1{\def\@supplement{#1}}
+\let\@supplement\@empty
+\define@key{supplementdetails}{linktext}{\def\supplementdetails@linktext{#1}}
+\define@key{supplementdetails}{cite}{\def\supplementdetails@cite{#1}}
+\define@key{supplementdetails}{subcategory}{\def\supplementdetails@subcategory{#1}}
+\define@key{supplementdetails}{swhlinktext}{\def\supplementdetails@swhlinktext{#1}}
+\let\supplementdetails@swhlinktext\@empty
+\define@key{supplementdetails}{swhid}{
+ \ifx\supplementdetails@swhlinktext\@empty%
+ \StrBefore{#1}{;}[\supplementdetails@swhlinktext]%
+ \fi%
+ \def\supplementdetails@swhid{#1}%
+}
+
+\define@key{supplementdetails}{swhdelimiter}{\def\supplementdetails@swhdelimiter{#1}}
+\def\supplementdetails@swhdelimiter{\\ \hspace*{1.2em}}
+\newcommand*\addtosupplementmacro[2]{%
+ \ifx\@supplement\@empty%
+ \g@addto@macro\@supplement{#1}%
+ \else%
+ \g@addto@macro\@supplement{\\#1}%
+ \fi%
+}%
+\newcommand{\supplementdetails}[3][]{%
+ \begingroup%
+ \let\supplementdetails@linktext\@empty
+ \let\supplementdetails@cite\@empty
+ \let\supplementdetails@subcategory\@empty
+ \let\supplementdetails@swhid\@empty
+ \setkeys{supplementdetails}{#1}%
+ \ifx\supplementdetails@subcategory\@empty%
+ \protected@edef\tmp{\textit{#2}}
+ \else
+ \protected@edef\tmp{\textit{#2\,\,(\supplementdetails@subcategory)}}%
+ \fi
+ \ifx\supplementdetails@linktext\@empty%
+ \protected@edef\tmp{\tmp:\space{\url{#3}}}%
+ \else%
+ \protected@edef\tmp{\tmp:\space{\href{#3}{\texttt{\supplementdetails@linktext}}}}%
+ \fi%
+ \ifx\supplementdetails@cite\@empty%
+ \else%
+ \protected@edef\tmp{\tmp\nobreakspace\cite{\supplementdetails@cite}}%
+ \fi
+ \ifx\supplementdetails@swhid\@empty%
+ \else%
+ \ifx\supplementdetails@swhlinktext\@empty%
+ \protected@edef\tmp{\tmp \supplementdetails@swhdelimiter{} archived at %
+ \href{https://archive.softwareheritage.org/\supplementdetails@swhid}{\nolinkurl{\supplementdetails@swhid}}}%
+ \else%
+ \protected@edef\tmp{\tmp \supplementdetails@swhdelimiter{} archived at %
+ \href{https://archive.softwareheritage.org/\supplementdetails@swhid}{\nolinkurl{\supplementdetails@swhlinktext}}}%
+ \fi%
+ \fi%
+ \expandafter\addtosupplementmacro\expandafter{\tmp}{#1}%
+ \endgroup%
+}%
+\def\supplementHeading{%
+ \textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries
+ Supplementary Material\enskip}}
+\newcommand\flag[2][0.9cm]{%
+ \leavevmode\marginpar{%
+ \raisebox{\dimexpr-\totalheight+\ht\strutbox\relax}%
+ [\dimexpr\ht\strutbox+3mm][\dp\strutbox]{\expandafter\includegraphics[width=#1]{#2}}%
+}}
+\def\funding#1{\def\@funding{#1}}
+\let\@funding\@empty
+\def\fundingHeading{%
+ \textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries
+ Funding\enskip}}
+\def\acknowledgements#1{\def\@acknowledgements{#1}}
+\let\@acknowledgements\@empty
+\def\acknowledgementsHeading{%
+ \textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries
+ Acknowledgements\enskip}}
+\RequirePackage{amsthm}
+\ifx\usethmrestate\relax
+ \RequirePackage{thm-restate}
+\fi
+\thm@headfont{%
+ \textcolor{lipicsGray}{$\blacktriangleright$}\nobreakspace\sffamily\bfseries}
+\def\th@remark{%
+ \thm@headfont{%
+ \textcolor{lipicsGray}{$\blacktriangleright$}\nobreakspace\sffamily}%
+ \normalfont % body font
+ \thm@preskip\topsep \divide\thm@preskip\tw@
+ \thm@postskip\thm@preskip
+}
+\def\@endtheorem{\endtrivlist}%\@endpefalse
+\renewcommand\qedsymbol{\textcolor{lipicsGray}{\ensuremath{\blacktriangleleft}}}
+\renewenvironment{proof}[1][\proofname]{\par
+ \pushQED{\qed}%
+ \normalfont \topsep6\p@\@plus6\p@\relax
+ \trivlist
+ \item[\hskip\labelsep
+ \color{lipicsGray}\sffamily\bfseries
+ #1\@addpunct{.}]\ignorespaces
+}{%
+ \popQED\endtrivlist%\@endpefalse
+}
+\newcommand{\claimqedhere}{\renewcommand\qedsymbol{\textcolor{lipicsGray}{\ensuremath{\vartriangleleft}}}%
+\qedhere%
+\renewcommand\qedsymbol{\textcolor{lipicsGray}{\ensuremath{\blacktriangleleft}}}}
+\newenvironment{claimproof}[1][\proofname]{
+ \pushQED{\qed}%
+ \normalfont \topsep6\p@\@plus6\p@\relax
+ \trivlist
+ \item[\hskip\labelsep
+ \color{lipicsGray}\sffamily
+ #1\@addpunct{.}]\ignorespaces
+}{%
+ \renewcommand\qedsymbol{\textcolor{lipicsGray}{\ensuremath{\vartriangleleft}}}
+ \popQED\endtrivlist%\@endpefalse
+ \renewcommand\qedsymbol{\textcolor{lipicsGray}{\ensuremath{\blacktriangleleft}}}
+}
+% inspired by qed of amsthm class
+\DeclareRobustCommand{\lipicsEnd}{%
+ \leavevmode\unskip\penalty9999 \hbox{}\nobreak\hfill
+ \quad\hbox{$\lrcorner$}%
+}
+\AtBeginDocument{
+ \@ifpackageloaded{algorithm2e}{
+ \@ifpackagelater{algorithm2e}{2009/11/17}{
+ \renewcommand{\algorithmcfname}{\sffamily\bfseries{}Algorithm}%
+ \renewcommand{\@algocf@procname}{\sffamily\bfseries{}Procedure}%
+ \SetAlgoCaptionSeparator{~}
+ \SetAlCapHSkip{0pt}
+ \renewcommand{\algocf@captiontext}[2]{%
+ \kern0.05em{\color{lipicsYellow}\rule{0.73em}{0.73em}}%
+ \hspace*{0.67em}\small #1\algocf@capseparator\nobreakspace#2}
+ \renewcommand{\algocf@makecaption}[2]{%
+ \parbox[t]{\textwidth}{\algocf@captiontext{#1}{#2}}%
+ }%
+ \renewcommand{\algocf@captionproctext}[2]{%
+ {%
+ \kern0.05em{\color{lipicsYellow}\rule{0.73em}{0.73em}}%
+ \hspace*{0.67em}\small%
+\ProcSty{\ProcFnt\algocf@procname\ifthenelse{\boolean{algocf@procnumbered}}{\nobreakspace\thealgocf\algocf@typo\algocf@capseparator}{\relax}}%
+ \nobreakspace\ProcNameSty{\ProcNameFnt\algocf@captname #2@}% Name of the procedure in ProcName Style.
+ \ifthenelse{\equal{\algocf@captparam #2@}{\arg@e}}{}{% if no argument, write nothing
+ \ProcNameSty{\ProcNameFnt(}\ProcArgSty{\ProcArgFnt\algocf@captparam #2@}\ProcNameSty{\ProcNameFnt)}%else put arguments in ProcArgSty:
+ }% endif
+ \algocf@captother #2@%
+ }%
+}%
+ \renewcommand{\@algocf@capt@boxed}{above}
+ \renewcommand{\@algocf@capt@ruled}{above}
+ \setlength\algotitleheightrule{0pt}
+ }{\ClassWarning{%
+ Package algorithm2e outdated}{You are using an outdated version of the package algorithm2e. Please update!}}
+ }{}
+ \@ifpackageloaded{algorithm}{
+ \captionsetup[algorithm]{name=Algorithm, labelformat=boxed, position=top}
+ \newcommand\fs@ruled@notop{\def\@fs@cfont{\bfseries}\let\@fs@capt\floatc@ruled
+ \def\@fs@pre{}%
+ \def\@fs@post{\kern2pt\hrule\relax}%
+ \def\@fs@mid{\kern2pt\hrule\kern2pt}%
+ \let\@fs@iftopcapt\iftrue}
+ \@ifundefined{fst@algorithm}{}{
+ \renewcommand\fst@algorithm{\fs@ruled@notop}
+ }
+ }{}
+ \ifx\usecleveref\relax\else
+ \@ifpackageloaded{cleveref}{\ClassWarning{Use document option 'cleveref' instead}{Use document option 'cleveref' instead directly loading package 'cleveref'}}{}
+ \fi
+ \ifx\usethmrestate\relax\else
+ \@ifpackageloaded{thm-restate}{\ClassWarning{Use document option 'thm-restate' instead}{Use document option 'thm-restate' instead directly loading package 'thm-restate'}}{}
+ \fi
+ \ifx\useautoref\relax
+ \@ifundefined{algorithmautorefname}{\newcommand{\algorithmautorefname}{Algorithm}}{\renewcommand{\algorithmautorefname}{Algorithm}}%
+ \fi
+}
+
+\ifx\usecleveref\relax
+ \RequirePackage[capitalise, noabbrev]{cleveref}
+ \crefname{algocf}{Algorithm}{Algorithms}
+ \Crefname{algocf}{Algorithm}{Algorithms}
+ \newcommand{\crefrangeconjunction}{--}
+ \newcommand{\creflastconjunction}{, and\nobreakspace}
+\fi
+\ifx\useautoref\relax
+ \RequirePackage{aliascnt}
+\fi
+\newtheoremstyle{claimstyle}{\topsep}{\topsep}{}{0pt}{\sffamily}{. }{5pt plus 1pt minus 1pt}%
+ {$\vartriangleright$ \thmname{#1}\thmnumber{ #2}\thmnote{ (#3)}}
+\theoremstyle{plain}
+\newtheorem{theorem}{Theorem}
+\ifx\numberwithinsect\relax
+ \@addtoreset{theorem}{section}
+ \expandafter\def\expandafter\thetheorem\expandafter{%
+ \expandafter\thesection\expandafter\@thmcountersep\thetheorem}
+\fi
+
+\ifx\useautoref\relax
+ \addto\extrasenglish{%
+ \def\chapterautorefname{Chapter}%
+ \def\sectionautorefname{Section}%
+ \def\subsectionautorefname{Subsection}%
+ \def\subsubsectionautorefname{Subsubsection}%
+ \def\paragraphautorefname{Paragraph}%
+ \def\subparagraphautorefname{Subparagraph}%
+ }
+ \addto\extrasUKenglish{%
+ \def\chapterautorefname{Chapter}%
+ \def\sectionautorefname{Section}%
+ \def\subsectionautorefname{Subsection}%
+ \def\subsubsectionautorefname{Subsubsection}%
+ \def\paragraphautorefname{Paragraph}%
+ \def\subparagraphautorefname{Subparagraph}%
+ }
+ \addto\extrasUSenglish{%
+ \def\chapterautorefname{Chapter}%
+ \def\sectionautorefname{Section}%
+ \def\subsectionautorefname{Subsection}%
+ \def\subsubsectionautorefname{Subsubsection}%
+ \def\paragraphautorefname{Paragraph}%
+ \def\subparagraphautorefname{Subparagraph}%
+ }
+ \ifx\usethmrestate\relax
+ \newtheorem{lemma}[theorem]{Lemma}
+ \newtheorem{corollary}[theorem]{Corollary}
+ \newtheorem{proposition}[theorem]{Proposition}
+ \newtheorem{exercise}[theorem]{Exercise}
+ \newtheorem{definition}[theorem]{Definition}
+ \newtheorem{conjecture}[theorem]{Conjecture}
+ \newtheorem{observation}[theorem]{Observation}
+ \theoremstyle{definition}
+ \newtheorem{example}[theorem]{Example}
+ \theoremstyle{remark}
+ \newtheorem{note}[theorem]{Note}
+ \newtheorem*{note*}{Note}
+ \newtheorem{remark}[theorem]{Remark}
+ \newtheorem*{remark*}{Remark}
+ \theoremstyle{claimstyle}
+ \newtheorem{claim}[theorem]{Claim}
+ \newtheorem*{claim*}{Claim}
+ \else
+ \newaliascnt{lemma}{theorem}
+ \newtheorem{lemma}[lemma]{Lemma}
+ \aliascntresetthe{lemma}
+ \newcommand{\lemmaautorefname}{Lemma}
+ \newaliascnt{corollary}{theorem}
+ \newtheorem{corollary}[corollary]{Corollary}
+ \aliascntresetthe{corollary}
+ \newcommand{\corollaryautorefname}{Corollary}
+ \newaliascnt{proposition}{theorem}
+ \newtheorem{proposition}[proposition]{Proposition}
+ \aliascntresetthe{proposition}
+ \newcommand{\propositionautorefname}{Proposition}
+ \newaliascnt{exercise}{theorem}
+ \newtheorem{exercise}[exercise]{Exercise}
+ \aliascntresetthe{exercise}
+ \newcommand{\exerciseautorefname}{Exercise}
+ \newaliascnt{definition}{theorem}
+ \newtheorem{definition}[definition]{Definition}
+ \aliascntresetthe{definition}
+ \newcommand{\definitionautorefname}{Definition}
+ \newaliascnt{conjecture}{theorem}
+ \newtheorem{conjecture}[conjecture]{Conjecture}
+ \aliascntresetthe{conjecture}
+ \newcommand{\conjectureautorefname}{Conjecture}
+ \newaliascnt{observation}{theorem}
+ \newtheorem{observation}[observation]{Observation}
+ \aliascntresetthe{observation}
+ \newcommand{\observationautorefname}{Observation}
+ \theoremstyle{definition}
+ \newaliascnt{example}{theorem}
+ \newtheorem{example}[example]{Example}
+ \aliascntresetthe{example}
+ \newcommand{\exampleautorefname}{Example}
+ \theoremstyle{remark}
+ \newaliascnt{note}{theorem}
+ \newtheorem{note}[note]{Note}
+ \aliascntresetthe{note}
+ \newcommand{\noteautorefname}{Note}
+ \newtheorem*{note*}{Note}
+ \newaliascnt{remark}{theorem}
+ \newtheorem{remark}[remark]{Remark}
+ \aliascntresetthe{remark}
+ \newcommand{\remarkautorefname}{Remark}
+ \newtheorem*{remark*}{Remark}
+ \theoremstyle{claimstyle}
+ \newaliascnt{claim}{theorem}
+ \newtheorem{claim}[claim]{Claim}
+ \aliascntresetthe{claim}
+ \newcommand{\claimautorefname}{Claim}
+ \newtheorem*{claim*}{Claim}
+ \fi
+\else
+ \newtheorem{lemma}[theorem]{Lemma}
+ \newtheorem{corollary}[theorem]{Corollary}
+ \newtheorem{proposition}[theorem]{Proposition}
+ \newtheorem{exercise}[theorem]{Exercise}
+ \newtheorem{definition}[theorem]{Definition}
+ \newtheorem{conjecture}[theorem]{Conjecture}
+ \newtheorem{observation}[theorem]{Observation}
+ \theoremstyle{definition}
+ \newtheorem{example}[theorem]{Example}
+ \theoremstyle{remark}
+ \newtheorem{note}[theorem]{Note}
+ \newtheorem*{note*}{Note}
+ \newtheorem{remark}[theorem]{Remark}
+ \newtheorem*{remark*}{Remark}
+ \theoremstyle{claimstyle}
+ \newtheorem{claim}[theorem]{Claim}
+ \newtheorem*{claim*}{Claim}
+\fi
+\theoremstyle{plain}
+\endinput
+%%
+%% End of file `lipics-v2021.cls'.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Paper/document/root.bib Tue Jan 25 13:12:50 2022 +0000
@@ -0,0 +1,340 @@
+@article{HosoyaVouillonPierce2005,
+ author = {H.~Hosoya and J.~Vouillon and B.~C.~Pierce},
+ title = {{R}egular {E}xpression {T}ypes for {XML}},
+ journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
+ year = {2005},
+ volume = 27,
+ number = 1,
+ pages = {46--90}
+}
+
+
+@Misc{POSIX,
+ title = {{T}he {O}pen {G}roup {B}ase {S}pecification {I}ssue 6 {IEEE} {S}td 1003.1 2004 {E}dition},
+ year = {2004},
+ note = {\url{http://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap09.html}}
+}
+
+
+@InProceedings{AusafDyckhoffUrban2016,
+ author = {F.~Ausaf and R.~Dyckhoff and C.~Urban},
+ title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions ({P}roof {P}earl)},
+ year = {2016},
+ booktitle = {Proc.~of the 7th International Conference on Interactive Theorem Proving (ITP)},
+ volume = {9807},
+ series = {LNCS},
+ pages = {69--86}
+}
+
+@article{aduAFP16,
+ author = {F.~Ausaf and R.~Dyckhoff and C.~Urban},
+ title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions},
+ journal = {Archive of Formal Proofs},
+ year = 2016,
+ note = {\url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}, Formal proof development},
+ ISSN = {2150-914x}
+}
+
+
+@TechReport{CrashCourse2014,
+ author = {N.~B.~B.~Grathwohl and F.~Henglein and U.~T.~Rasmussen},
+ title = {{A} {C}rash-{C}ourse in {R}egular {E}xpression {P}arsing and {R}egular
+ {E}xpressions as {T}ypes},
+ institution = {University of Copenhagen},
+ year = {2014},
+ annote = {draft report}
+}
+
+@inproceedings{Sulzmann2014,
+ author = {M.~Sulzmann and K.~Lu},
+ title = {{POSIX} {R}egular {E}xpression {P}arsing with {D}erivatives},
+ booktitle = {Proc.~of the 12th International Conference on Functional and Logic Programming (FLOPS)},
+ pages = {203--220},
+ year = {2014},
+ volume = {8475},
+ series = {LNCS}
+}
+
+@inproceedings{Sulzmann2014b,
+ author = {M.~Sulzmann and P.~van Steenhoven},
+ title = {{A} {F}lexible and {E}fficient {ML} {L}exer {T}ool {B}ased on {E}xtended {R}egular
+ {E}xpression {S}ubmatching},
+ booktitle = {Proc.~of the 23rd International Conference on Compiler Construction (CC)},
+ pages = {174--191},
+ year = {2014},
+ volume = {8409},
+ series = {LNCS}
+}
+
+@book{Pierce2015,
+ author = {B.~C.~Pierce and C.~Casinghino and M.~Gaboardi and
+ M.~Greenberg and C.~Hri\c{t}cu and
+ V.~Sj\"{o}berg and B.~Yorgey},
+ title = {{S}oftware {F}oundations},
+ year = {2015},
+ publisher = {Electronic textbook},
+ note = {\url{http://www.cis.upenn.edu/~bcpierce/sf}}
+}
+
+@Misc{Kuklewicz,
+ author = {C.~Kuklewicz},
+ title = {{R}egex {P}osix},
+ howpublished = "\url{https://wiki.haskell.org/Regex_Posix}"
+}
+
+@article{Vansummeren2006,
+ author = {S.~Vansummeren},
+ title = {{T}ype {I}nference for {U}nique {P}attern {M}atching},
+ year = {2006},
+ journal = {ACM Transactions on Programming Languages and Systems},
+ volume = {28},
+ number = {3},
+ pages = {389--428}
+}
+
+@InProceedings{Asperti12,
+ author = {A.~Asperti},
+ title = {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence},
+ booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving (ITP)},
+ pages = {283--298},
+ year = {2012},
+ volume = {7406},
+ series = {LNCS}
+}
+
+@inproceedings{Frisch2004,
+ author = {A.~Frisch and L.~Cardelli},
+ title = {{G}reedy {R}egular {E}xpression {M}atching},
+ booktitle = {Proc.~of the 31st International Conference on Automata, Languages and Programming (ICALP)},
+ pages = {618--629},
+ year = {2004},
+ volume = {3142},
+ series = {LNCS}
+}
+
+@ARTICLE{Antimirov95,
+ author = {V.~Antimirov},
+ title = {{P}artial {D}erivatives of {R}egular {E}xpressions and
+ {F}inite {A}utomata {C}onstructions},
+ journal = {Theoretical Computer Science},
+ year = {1995},
+ volume = {155},
+ pages = {291--319}
+}
+
+@inproceedings{Nipkow98,
+ author={T.~Nipkow},
+ title={{V}erified {L}exical {A}nalysis},
+ booktitle={Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs)},
+ series={LNCS},
+ volume=1479,
+ pages={1--15},
+ year=1998
+}
+
+@article{Brzozowski1964,
+ author = {J.~A.~Brzozowski},
+ title = {{D}erivatives of {R}egular {E}xpressions},
+ journal = {Journal of the {ACM}},
+ volume = {11},
+ number = {4},
+ pages = {481--494},
+ year = {1964}
+}
+
+@article{Leroy2009,
+ author = {X.~Leroy},
+ title = {{F}ormal {V}erification of a {R}ealistic {C}ompiler},
+ journal = {Communications of the ACM},
+ year = 2009,
+ volume = 52,
+ number = 7,
+ pages = {107--115}
+}
+
+@InProceedings{Paulson2015,
+ author = {L.~C.~Paulson},
+ title = {{A} {F}ormalisation of {F}inite {A}utomata {U}sing {H}ereditarily {F}inite {S}ets},
+ booktitle = {Proc.~of the 25th International Conference on Automated Deduction (CADE)},
+ pages = {231--245},
+ year = {2015},
+ volume = {9195},
+ series = {LNAI}
+}
+
+@Article{Wu2014,
+ author = {C.~Wu and X.~Zhang and C.~Urban},
+ title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions},
+ journal = {Journal of Automatic Reasoning},
+ year = {2014},
+ volume = {52},
+ number = {4},
+ pages = {451--480}
+}
+
+@InProceedings{Regehr2011,
+ author = {X.~Yang and Y.~Chen and E.~Eide and J.~Regehr},
+ title = {{F}inding and {U}nderstanding {B}ugs in {C} {C}ompilers},
+ pages = {283--294},
+ year = {2011},
+ booktitle = {Proc.~of the 32nd ACM SIGPLAN Conference on Programming Language Design and
+ Implementation (PLDI)}
+}
+
+@Article{Norrish2014,
+ author = {A.~Barthwal and M.~Norrish},
+ title = {{A} {M}echanisation of {S}ome {C}ontext-{F}ree {L}anguage {T}heory in {HOL4}},
+ journal = {Journal of Computer and System Sciences},
+ year = {2014},
+ volume = {80},
+ number = {2},
+ pages = {346--362}
+}
+
+@Article{Thompson1968,
+ author = {K.~Thompson},
+ title = {{P}rogramming {T}echniques: {R}egular {E}xpression {S}earch {A}lgorithm},
+ journal = {Communications of the ACM},
+ issue_date = {June 1968},
+ volume = {11},
+ number = {6},
+ year = {1968},
+ pages = {419--422}
+}
+
+@article{Owens2009,
+ author = {S.~Owens and J.~H.~Reppy and A.~Turon},
+ title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined},
+ journal = {Journal of Functinal Programming},
+ volume = {19},
+ number = {2},
+ pages = {173--190},
+ year = {2009}
+}
+
+@inproceedings{Sulzmann2015,
+ author = {M.~Sulzmann and P.~Thiemann},
+ title = {{D}erivatives for {R}egular {S}huffle {E}xpressions},
+ booktitle = {Proc.~of the 9th International Conference on Language and Automata Theory
+ and Applications (LATA)},
+ pages = {275--286},
+ year = {2015},
+ volume = {8977},
+ series = {LNCS}
+}
+
+@inproceedings{Chen2012,
+ author = {H.~Chen and S.~Yu},
+ title = {{D}erivatives of {R}egular {E}xpressions and an {A}pplication},
+ booktitle = {Proc.~in the International Workshop on Theoretical
+ Computer Science (WTCS)},
+ pages = {343--356},
+ year = {2012},
+ volume = {7160},
+ series = {LNCS}
+}
+
+@article{Krauss2011,
+ author={A.~Krauss and T.~Nipkow},
+ title={{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra},
+ journal={Journal of Automated Reasoning},
+ volume=49,
+ pages={95--106},
+ year=2012
+}
+
+@InProceedings{Traytel2015,
+ author = {D.~Traytel},
+ title = {{A} {C}oalgebraic {D}ecision {P}rocedure for {WS1S}},
+ booktitle = {Proc.~of the 24th Annual Conference on Computer Science Logic (CSL)},
+ pages = {487--503},
+ series = {LIPIcs},
+ year = {2015},
+ volume = {41}
+}
+
+@inproceedings{Traytel2013,
+ author={D.~Traytel and T.~Nipkow},
+ title={{A} {V}erified {D}ecision {P}rocedure for {MSO} on
+ {W}ords {B}ased on {D}erivatives of {R}egular {E}xpressions},
+ booktitle={Proc.~of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP)},
+ pages={3-12},
+ year=2013
+}
+
+@InProceedings{Coquand2012,
+ author = {T.~Coquand and V.~Siles},
+ title = {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory},
+ booktitle = {Proc.~of the 1st International Conference on Certified Programs and Proofs (CPP)},
+ pages = {119--134},
+ year = {2011},
+ volume = {7086},
+ series = {LNCS}
+}
+
+@InProceedings{Almeidaetal10,
+ author = {J.~B.~Almeida and N.~Moriera and D.~Pereira and S.~M.~de Sousa},
+ title = {{P}artial {D}erivative {A}utomata {F}ormalized in {C}oq},
+ booktitle = {Proc.~of the 15th International Conference on Implementation
+ and Application of Automata (CIAA)},
+ pages = {59-68},
+ year = {2010},
+ volume = {6482},
+ series = {LNCS}
+}
+
+@article{Owens2008,
+ author = {S.~Owens and K.~Slind},
+ title = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic},
+ journal = {Higher-Order and Symbolic Computation},
+ volume = {21},
+ number = {4},
+ year = {2008},
+ pages = {377--409}
+}
+
+
+@article{Owens2,
+ author = {S.~Owens and K.~Slind},
+ title = {Adapting functional programs to higher order logic},
+ journal = {Higher-Order and Symbolic Computation},
+ volume = {21},
+ number = {4},
+ pages = {377--409},
+ year = {2008},
+ url = {http://dx.doi.org/10.1007/s10990-008-9038-0},
+ doi = {10.1007/s10990-008-9038-0},
+ timestamp = {Wed, 16 Dec 2009 13:51:02 +0100},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/lisp/OwensS08},
+ bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+@misc{PCRE,
+ title = "{PCRE - Perl Compatible Regular Expressions}",
+ url = {http://www.pcre.org},
+}
+
+
+
+@InProceedings{OkuiSuzuki2010,
+ author = {S.~Okui and T.~Suzuki},
+ title = {{D}isambiguation in {R}egular {E}xpression {M}atching via
+ {P}osition {A}utomata with {A}ugmented {T}ransitions},
+ booktitle = {Proc.~of the 15th International Conference on Implementation
+ and Application of Automata (CIAA)},
+ year = {2010},
+ volume = {6482},
+ series = {LNCS},
+ pages = {231--240}
+}
+
+
+
+@TechReport{OkuiSuzukiTech,
+ author = {S.~Okui and T.~Suzuki},
+ title = {{D}isambiguation in {R}egular {E}xpression {M}atching via
+ {P}osition {A}utomata with {A}ugmented {T}ransitions},
+ institution = {University of Aizu},
+ year = {2013}
+}
+