\documentclass{llncs}
\usepackage[utf8]{inputenc}
\usepackage{lineno}
\usepackage{url}
\usepackage{amsmath,amssymb}
\usepackage{isabelle,isabellesym}
\usepackage{pdfsetup}
\usepackage{ot1patch}
%\usepackage{boxedminipage}

\allowdisplaybreaks
\urlstyle{rm}
\isabellestyle{it}
\renewcommand{\isastyleminor}{\it}%
\renewcommand{\isastyle}{\normalsize\it}%

\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
\renewcommand{\isasymbullet}{{\raisebox{0.2mm}{\small$\bullet$}}}
\renewcommand{\isasymintegral}{$\lambda$}
\renewcommand{\isasymlbrace}{$\ulcorner$}
\renewcommand{\isasymrbrace}{$\urcorner$}
%\renewcommand{\isasymguillemotleft}{}
%\renewcommand{\isasymguillemotright}{}

\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
\renewcommand{\isasymequiv}{=}
%%\renewcommand{\isasymiota}{}
\renewcommand{\isasymxi}{$..$}
\renewcommand{\isasymemptyset}{$\varnothing$}
\newcommand{\isasymnotapprox}{$\not\approx$}
\newcommand{\isasymLET}{$\mathtt{let}$}
\newcommand{\isasymAND}{$\mathtt{and}$}
\newcommand{\isasymIN}{$\mathtt{in}$}
\newcommand{\isasymEND}{$\mathtt{end}$}
\newcommand{\isasymBIND}{$\mathtt{bind}$}
\newcommand{\isasymANIL}{$\mathtt{anil}$}
\newcommand{\isasymACONS}{$\mathtt{acons}$}
\newcommand{\isasymCASE}{$\mathtt{case}$}
\newcommand{\isasymOF}{$\mathtt{of}$}
\newcommand{\isasymAL}{\makebox[0mm][l]{$^\alpha$}}
\newcommand{\isasymPRIME}{\makebox[0mm][l]{$'$}}
\newcommand{\isasymFRESH}{\#}
\newcommand{\LET}{\;\mathtt{let}\;}
\newcommand{\IN}{\;\mathtt{in}\;}
\newcommand{\END}{\;\mathtt{end}\;}
\newcommand{\AND}{\;\mathtt{and}\;}
\newcommand{\fv}{\mathit{fv}}

\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}

\begin{document}

\title{Execution modulo alpha-equivalence}
\author{...\inst{1} \and ...\inst{2}}
\institute{... \and ...}

\maketitle

\begin{abstract}
  In this paper we show how a formal specification defined modulo
  alpha-equivalence can be programatically made executable.
  We show a general algorithm and we present examples of
  executed calculi, which we implement in Nominal Isabelle.
\end{abstract}

\input{session}

%\begin{spacing}{0.9}
\bibliographystyle{abbrv}
\bibliography{root}
%\end{spacing}

\end{document}

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