\documentclass{llncs}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{tikz}
\usepackage{pgf}
\usepackage{pdfsetup}
\usepackage{ot1patch}
\usepackage{times}
\usepackage{proof}
\usepackage{stmaryrd}

\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{$\_\!\_$}}

\newcommand{\isasymcalL}{\ensuremath{\cal{L}}}
\begin{document}

\title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular
  Expressions (Proof Pearl)}
\author{Chunhan Wu\inst{1} \and Xingjuan Zhang\inst{1} \and Christian Urban\inst{2}}
\institute{PLA University, China \and TU Munich, Germany}
\maketitle

\begin{abstract} 
There are numerous textbooks on regular languages. Nearly all of them 
introduce the subject by describing finite automata and 
only mentioning on the side a connection with regular expressions. 
Unfortunately, automata are a hassle for formalisations in HOL-based
theorem provers. The reason is that they need to be represented as graphs, 
matrices or functions, none of which are inductive datatypes. Also 
operations, such as disjoint unions of graphs, are not easily formalisiable 
in HOL. In contrast, regular expressions can be defined conveniently 
as datatype and a corresponding reasoning infrastructure comes for 
free. We show in this paper that a central result from formal 
language theory---the Myhill-Nerode theorem---can be recreated 
using only regular expressions. 
\end{abstract}


\input{session}

\bibliographystyle{plain}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: