%\documentclass{svjour3}+ −
\documentclass{llncs}+ −
\usepackage{times}+ −
\usepackage{isabelle}+ −
\usepackage{isabellesym}+ −
\usepackage{amsmath}+ −
\usepackage{amssymb}+ −
\usepackage{pdfsetup}+ −
\usepackage{tikz}+ −
\usepackage{pgf}+ −
\usepackage{verbdef}+ −
\usepackage{longtable}+ −
\usepackage{mathpartir}+ −
+ −
\urlstyle{rm}+ −
\isabellestyle{it}+ −
\renewcommand{\isastyle}{\isastyleminor}+ −
+ −
\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}+ −
+ −
\title{Quotients Revisited for Isabelle/HOL}+ −
\author{Cezary Kaliszyk$^*$ and Christian Urban$^*$}+ −
\institute{$^*$ Technical University of Munich, Germany}+ −
\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}+ −
+ −
% generated text of all theories+ −
\input{session}+ −
+ −
% optional bibliography+ −
\bibliographystyle{abbrv}+ −
\bibliography{root}+ −
+ −
\end{document}+ −
+ −
%%% Local Variables:+ −
%%% mode: latex+ −
%%% TeX-master: t+ −
%%% End:+ −