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

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

\renewcommand{\isamarkupchapter}[1]{\section{#1}}
\renewcommand{\isamarkupsection}[1]{\subsection{#1}}
\renewcommand{\isamarkupsubsection}[1]{\subsubsection{#1}}
\renewcommand{\isamarkupsubsubsection}[1]{\paragraph{#1}}



\begin{document}

\title{Deriving generic class instances for datatypes}
\author{Jonas Rädle and Lars Hupel}
\maketitle

\begin{abstract}
We provide a framework for automatically deriving instances for generic type classes. Our approach is inspired by
Haskell's \textit{generic-deriving} package \cite{magalhaes2010generic} and Scala's \textit{shapeless} library \cite{shapeless2018}.

In addition to generating the code for type class functions, we also attempt to automatically prove type class laws for these instances. 
As of now, however, some manual proofs are still required for recursive datatypes.
\end{abstract}

\tableofcontents

% include generated text of all theories
\input{session}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}
