\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}

\usepackage[english]{babel}

% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

\usepackage{amsmath}
\usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

\usepackage{wasysym}

%\usepackage{eurosym}
  %for \<euro>

\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{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{Effect Polymorphism in Higher-Order Logic}
\author{Andreas Lochbihler}
\maketitle

\begin{abstract}
  The notion of a \emph{monad} cannot be expressed within higher-order logic (HOL) due to type system restrictions.
  We show that if a monad is used with values of only one type, this notion \emph{can} be formalised in HOL.
  Based on this idea, we develop a library of effect specifications and implementations of monads and monad transformers.
  Hence, we can abstract over the concrete monad in HOL definitions and thus use the same definition for different (combinations of) effects.
  We illustrate the usefulness of effect polymorphism with a monadic interpreter for a simple language.
\end{abstract}

\tableofcontents

\newpage

% 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:
