\documentclass{sig-alternate}
  \pdfpagewidth=8.5truein
  \pdfpageheight=11truein
\usepackage{times}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{pdfsetup}
\usepackage{tikz}
\usepackage{pgf}
\usepackage{verbdef}
\usepackage{longtable}
\usepackage{mathpartir}
\newtheorem{definition}{Definition}
\newtheorem{proposition}{Proposition}
\newtheorem{lemma}{Lemma}

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

\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
\verbdef\singlearr|--->|
\verbdef\doublearr|===>|
\verbdef\tripple|###|

\renewcommand{\isasymequiv}{$\dn$}
\renewcommand{\isasymemptyset}{$\varnothing$}
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
\renewcommand{\isasymUnion}{$\bigcup$}

\newcommand{\isasymsinglearr}{\singlearr}
\newcommand{\isasymdoublearr}{\doublearr}
\newcommand{\isasymtripple}{\tripple}

\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}

\begin{document}

\conferenceinfo{SAC'11}{March 21-25, 2011, TaiChung, Taiwan.}
\CopyrightYear{2011}
\crdata{978-1-4503-0113-8/11/03}

\title{Quotients Revisited for Isabelle/HOL}
\numberofauthors{2}
\author{
\alignauthor
Cezary Kaliszyk\\
  \affaddr{University of Tsukuba, Japan}\\
  \email{kaliszyk@score.cs.tsukuba.ac.jp}
\alignauthor
Christian Urban\\
  \affaddr{Technical University of Munich, Germany}\\
  \email{urbanc@in.tum.de}
}

\maketitle

\begin{abstract}
Higher-Order Logic (HOL) is based on a small logic kernel, whose only
mechanism for extension is the introduction of safe definitions and of
non-empty types. Both extensions are often performed in quotient
constructions. To ease the work involved with such quotient constructions, we
re-implemented in Isabelle/HOL the quotient package by Homeier. In doing so we
extended his work in order to deal with compositions of quotients. Like his
package, we designed our quotient package so that every step in a quotient construction
can be performed separately and as a result we are able to specify completely
the procedure of lifting theorems from the raw level to the quotient level.
The importance for programming language research is that many properties of
programming language calculi are easier to verify over $\alpha$-equated, or
$\alpha$-quotient, terms, than over raw terms.
\end{abstract}

\category{D.??}{TODO}{TODO}

\keywords{quotients, isabelle, higher order logic}

% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

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