\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{stmaryrd}

\usepackage{verbdef}

\usepackage{longtable}

\usepackage{mathpartir}

\newtheorem{definition}{Definition}

\newtheorem{proposition}{Proposition}

\newtheorem{lemma}{Lemma}

\urlstyle{rm}

\isabellestyle{rm}

\renewcommand{\isastyleminor}{\rm}%

\renewcommand{\isastyle}{\normalsize\rm}%

\renewcommand{\isastylescript}{\it}

\def\dn{\,\triangleq\,}

\verbdef\singlearr|---->|

\verbdef\doublearr|===>|

\verbdef\tripple|###|

\renewcommand{\isasymequiv}{$\triangleq$}

\renewcommand{\isasymemptyset}{$\varnothing$}

%%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}

\renewcommand{\isasymUnion}{$\bigcup$}

\newcommand{\isasymsinglearr}{$\mapsto$}

\newcommand{\isasymdoublearr}{$\Mapsto$}

\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@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 the %popular 

Isabelle/HOL theorem prover the quotient 

package by Homeier. In doing so we extended his work in order to deal with 

compositions of quotients and also specified completely the procedure 

of lifting theorems from the raw level to the quotient level.

The importance for theorem proving is that many formal

verifications, in order to be feasible, require a convenient reasoning infrastructure 

for quotient constructions.

\end{abstract}

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

\keywords{Quotients, Isabelle theorem prover, Higher-Order Logic}

% generated text of all theories

\bibliographystyle{abbrv}

\input{session}

\end{document}

%%% Local Variables:

%%% mode: latex

%%% TeX-master: t

%%% End: