diff -r 56057198e4f5 -r 70c10dc41606 thys3/document/root.tex --- a/thys3/document/root.tex Fri May 26 08:09:30 2023 +0100 +++ b/thys3/document/root.tex Fri May 26 08:10:17 2023 +0100 @@ -1,5 +1,5 @@ -\documentclass[runningheads]{llncs} -%!\documentclass[runningheads]{lipics-v2021} +%!\documentclass[runningheads]{llncs} +\documentclass[runningheads]{lipics-v2021} \usepackage{times} \usepackage{isabelle} \usepackage{isabellesym} @@ -53,6 +53,7 @@ \newcommand{\ZERO}{\mbox{\bf 0}} \newcommand{\ONE}{\mbox{\bf 1}} \def\rs{\mathit{rs}} +\definecolor{darkblue}{rgb}{0,0,0.6} \def\Brz{Brzozowski} \def\der{\backslash} @@ -62,11 +63,11 @@ %!\bibliographystyle{plainurl} \bibliographystyle{plain} -\title{{POSIX} {L}exing with {B}itcoded {D}erivatives} -\titlerunning{POSIX Lexing with Bitcoded Derivatives} -\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}} +%\title{{POSIX} {L}exing with {B}itcoded {D}erivatives} +%\titlerunning{POSIX Lexing with Bitcoded Derivatives} +%\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} @@ -78,6 +79,19 @@ %!\renewcommand{\DOIPrefix}{} %!\nolinenumbers +\title{{POSIX} {L}exing with {B}itcoded {D}erivatives} +\titlerunning{POSIX Lexing with Bitcoded Derivatives} +\author{Chengsong Tan}{Imperial College London}{ctan1@ic.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} \maketitle