%\documentclass{svjour3}+
−
\documentclass{llncs}+
−
\usepackage{times}+
−
\usepackage{isabelle}+
−
\usepackage{isabellesym}+
−
\usepackage{amsmath}+
−
\usepackage{amssymb}+
−
\usepackage{pdfsetup}+
−
+
−
+
−
\urlstyle{rm}+
−
\isabellestyle{it}+
−
\renewcommand{\isastyle}{\isastyleminor}+
−
+
−
\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}+
−
\renewcommand{\isasymequiv}{$\dn$}+
−
\renewcommand{\isasymemptyset}{$\varnothing$}+
−
+
−
\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), used in a number of theorem provers, is based on a small+
−
logic kernel, whose only mechanism for extension is the introduction of safe+
−
definitions and non-empty types. Both extensions are often performed by+
−
quotient constructions; for example finite sets are constructed by quotienting+
−
lists, or integers by quotienting pairs of natural numbers. To ease the work+
−
involved with 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. Also, we designed our quotient package so that+
−
every step in a quotient construction can be performed separately and as a+
−
result we were able to specify completely the procedure of lifting theorems from+
−
the raw level to the quotient level.  The importance to programming language+
−
research is that many properties of programming languages are more convenient+
−
to verify over $\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:+
−