\documentclass[10pt, conference, compsocconf]{IEEEtran}+
−
\usepackage{isabelle,isabellesym}+
−
+
−
%\usepackage{amssymb}+
−
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,+
−
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,+
−
  %\<triangleq>, \<yen>, \<lozenge>+
−
+
−
%\usepackage[greek,english]{babel}+
−
  %option greek for \<euro>+
−
  %option english (default language) for \<guillemotleft>, \<guillemotright>+
−
+
−
%\usepackage[only,bigsqcap]{stmaryrd}+
−
  %for \<Sqinter>+
−
+
−
%\usepackage{eufrak}+
−
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)+
−
+
−
%\usepackage{textcomp}+
−
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,+
−
  %\<currency>+
−
+
−
% this should be the last package used+
−
\usepackage{mathpartir}+
−
\usepackage{pdfsetup}+
−
+
−
% urls in roman style, theory text in math-similar italics+
−
\urlstyle{rm}+
−
\isabellestyle{it}+
−
+
−
% for uniform font size+
−
%\renewcommand{\isastyle}{\isastyleminor}+
−
+
−
+
−
\begin{document}+
−
+
−
\title{A Formalised Theory of Turing Machines in Isabelle/HOL}+
−
+
−
+
−
\author{+
−
\IEEEauthorblockN{Xu Jian, Xingyuan Zhang}+
−
\IEEEauthorblockA{PLA University of Science and Technology Nanjing, China}+
−
\and+
−
\IEEEauthorblockN{Christian Urban}+
−
\IEEEauthorblockA{King's College London, UK}+
−
}+
−
+
−
\maketitle+
−
+
−
+
−
\begin{abstract}+
−
Isabelle/HOL is an interactive theorem prover based on classical +
−
logic. While classical reasoning allow users to take convenient +
−
shortcuts in some proofs, it precludes \emph{direct} reasoning about +
−
decidability: every boolean predicate is either true or false+
−
because of the law of excluded middle. The only way to reason+
−
about decidability in a classical theorem prover, like Isabelle/HOL,+
−
is to formalise a concrete model for computation. In this paper+
−
we formalise Turing machines and relate them to register machines.+
−
+
−
\end{abstract}+
−
+
−
\begin{IEEEkeywords}+
−
Turing Machines, Decidability, Isabelle/HOL;+
−
\end{IEEEkeywords}+
−
+
−
+
−
\IEEEpeerreviewmaketitle+
−
+
−
+
−
%\tableofcontents+
−
+
−
% sane default for proof documents+
−
\parindent 0pt\parskip 0.5ex+
−
+
−
+
−
+
−
+
−
% generated text of all theories+
−
\input{session}+
−
+
−
% optional bibliography+
−
\bibliographystyle{abbrv}+
−
\bibliography{root}+
−
+
−
\end{document}+
−
+
−
%%% Local Variables:+
−
%%% mode: latex+
−
%%% TeX-master: t+
−
%%% End:+
−