\documentclass{entcs}  \usepackage{entcsmacro}
\usepackage{graphicx}
\sloppy

\usepackage{latexsym}
\usepackage{amsmath}
\usepackage{amssymb}

\usepackage{url}

\renewcommand{\today}{\number\day\ 
  \ifcase\month\or
  January\or February\or March\or April\or May\or June\or
  July\or August\or September\or October\or November\or December\fi
  \ \number\year}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preamble

\newcommand\cfile{}

\newcommand\comment[1]{} 
\newcommand\cc[1]{#1} % for label names 
% \renewcommand\footnote[1]{} % for footnotes
% \pagestyle{myheadings}
\pagestyle{plain} 

\renewcommand\theenumi{(\alph{enumi})}
\renewcommand\labelenumi{\theenumi}
\renewcommand\theenumii{(\roman{enumii})}
\renewcommand\labelenumii{\theenumii}

\newcommand\sfile[1]{\cite[\texttt{#1}]{l4-word-files}}
\newcommand\lenof{\texttt{len\_of}}
\newcommand\numof{\texttt{number\_of}}
\newcommand\TYPE{\texttt{TYPE}}
\newcommand\itself{\texttt{itself}}
\newcommand\False{\texttt{False}}
\newcommand\obin{\texttt{obin}}
\newcommand\bin{\texttt{bin}}
\newcommand\word{\texttt{word}}
\newcommand\arbitrary{\texttt{arbitrary}}
\newcommand\bintrunc{\texttt{bintrunc}}
\newcommand\norm{\texttt{norm}}
\newcommand\uint{\texttt{uint}}
\newcommand\sint{\texttt{sint}}
\newcommand\unat{\texttt{unat}}
\newcommand\Abs{\texttt{Abs}}
\newcommand\Rep{\texttt{Rep}}

\newcommand\set{\textit{set}}

\def\lastname{Dawson}

\begin{document}
\begin{frontmatter}
\title{Isabelle Theories for Machine Words}
  \author{Jeremy Dawson\thanksref{nicta}\thanksref{mywww}}
  \address{
Logic and Computation Program, NICTA \\
\and \\
Automated Reasoning Group,
\\ Australian National University,
 \\  Canberra, ACT 0200, Australia } 
\thanks[nicta]{National ICT Australia is funded by the Australian Government's
  Dept of Communications, Information Technology and the Arts and
  the Australian Research Council through Backing Australia's Ability
  and the ICT Centre of Excellence program.}
  \thanks[mywww]{
    \href{http://users.rsise.anu.edu.au/~jeremy/} 
    {\url{http://users.rsise.anu.edu.au/~jeremy/}}} 
\begin{abstract} 
  We describe a collection of Isabelle theories which facilitate reasoning
  about machine words.  For each possible word length, 
  the words of that length form a type,
  and most of our work consists of generic theorems which can be applied
  to any such type. 
  We develop the relationships between these words and integers (signed and
  unsigned), lists of booleans and functions from index to value,
  noting how these relationships are similar to those between an abstract type
  and its representing set.
  We discuss how we used Isabelle's {\tt bin} type,
  before and after it was changed
  from a datatype to an abstract type, and the techniques we used to retain,
  as nearly as possible, the convenience of primitive recursive definitions.
  We describe other useful techniques, 
  such as encoding the word length in the type.
\end{abstract}
\begin{keyword}
 machine words, twos-complement, mechanised reasoning
\end{keyword}
\end{frontmatter}

% ABOVE HERE SOME AWOCS (ENTCS) - SPECIFIC STUFF