--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotient-Paper/document/root-sac.tex	Thu Aug 19 15:02:11 2010 +0900
@@ -0,0 +1,92 @@
+\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: