1 \documentclass{sig-alternate}

     2   \pdfpagewidth=8.5truein

     3   \pdfpageheight=11truein

     4 \usepackage{times}

     5 \usepackage{isabelle}

     6 \usepackage{isabellesym}

     7 \usepackage{amsmath}

     8 \usepackage{amssymb}

     9 \usepackage{pdfsetup}

    10 \usepackage{tikz}

    11 \usepackage{pgf}

    12 \usepackage{verbdef}

    13 \usepackage{longtable}

    14 \usepackage{mathpartir}

    15 \newtheorem{definition}{Definition}

    16 \newtheorem{proposition}{Proposition}

    17 \newtheorem{lemma}{Lemma}

    18 

    19 \urlstyle{rm}

    20 \isabellestyle{it}

    21 \renewcommand{\isastyleminor}{\it}%

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

    23 

    24 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}

    25 \verbdef\singlearr|--->|

    26 \verbdef\doublearr|===>|

    27 \verbdef\tripple|###|

    28 

    29 \renewcommand{\isasymequiv}{$\dn$}

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

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

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

    33 

    34 \newcommand{\isasymsinglearr}{\singlearr}

    35 \newcommand{\isasymdoublearr}{\doublearr}

    36 \newcommand{\isasymtripple}{\tripple}

    37 

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

    39 

    40 \begin{document}

    41 

    42 \conferenceinfo{SAC'11}{March 21-25, 2011, TaiChung, Taiwan.}

    43 \CopyrightYear{2011}

    44 \crdata{978-1-4503-0113-8/11/03}

    45 

    46 \title{Quotients Revisited for Isabelle/HOL}

    47 \numberofauthors{2}

    48 \author{

    49 \alignauthor

    50 Cezary Kaliszyk\\

    51   \affaddr{University of Tsukuba, Japan}\\

    52   \email{kaliszyk@score.cs.tsukuba.ac.jp}

    53 \alignauthor

    54 Christian Urban\\

    55   \affaddr{Technical University of Munich, Germany}\\

    56   \email{urbanc@in.tum.de}

    57 }

    58 

    59 \maketitle

    60 

    61 \begin{abstract}

    62 Higher-Order Logic (HOL) is based on a small logic kernel, whose only

    63 mechanism for extension is the introduction of safe definitions and of

    64 non-empty types. Both extensions are often performed in quotient

    65 constructions. To ease the work involved with such quotient constructions, we

    66 re-implemented in Isabelle/HOL the quotient package by Homeier. In doing so we

    67 extended his work in order to deal with compositions of quotients. Like his

    68 package, we designed our quotient package so that every step in a quotient construction

    69 can be performed separately and as a result we are able to specify completely

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

    71 The importance for programming language research is that many properties of

    72 programming language calculi are easier to verify over $\alpha$-equated, or

    73 $\alpha$-quotient, terms, than over raw terms.

    74 \end{abstract}

    75 

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

    77 

    78 \keywords{quotients, isabelle, higher order logic}

    79 

    80 % generated text of all theories

    81 \input{session}

    82 

    83 % optional bibliography

    84 \bibliographystyle{abbrv}

    85 \bibliography{root}

    86 

    87 \end{document}

    88 

    89 %%% Local Variables:

    90 %%% mode: latex

    91 %%% TeX-master: t

    92 %%% End: