\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:+ −