--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/document/root.tex	Thu Nov 25 18:54:45 2010 +0000
@@ -0,0 +1,57 @@
+\documentclass{llncs}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{tikz}
+\usepackage{pgf}
+\usepackage{pdfsetup}
+\usepackage{ot1patch}
+\usepackage{times}
+\usepackage{proof}
+
+
+\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{$\_\!\_$}}
+
+\begin{document}
+
+\title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular Expressions}
+\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 they need to be represented as graphs 
+or matrices, neither of which can be easily defined as datatype. Also 
+operations, such as disjoint union of graphs, are not easily formalisiable 
+in HOL. In contrast, regular expressions can be defined easily 
+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: