nominal2: Quotient-Paper/document/root.tex@231a20534950 (annotated)

2174 157e8a4a6556 changed qpaper to lncs-style Christian Urban <urbanc@in.tum.de> parents: 2032 diff changeset	1	%\documentclass{svjour3}
157e8a4a6556 changed qpaper to lncs-style Christian Urban <urbanc@in.tum.de> parents: 2032 diff changeset	2	\documentclass{llncs}
1975 b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	\usepackage{times}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	\usepackage{isabelle}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	\usepackage{isabellesym}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	6	\usepackage{amsmath}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	\usepackage{amssymb}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	\usepackage{pdfsetup}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	9
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	10
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	\urlstyle{rm}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	\isabellestyle{it}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	\renewcommand{\isastyle}{\isastyleminor}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	14
2213 231a20534950 improved abstract, some tuning Christian Urban <urbanc@in.tum.de> parents: 2205 diff changeset	15	\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
231a20534950 improved abstract, some tuning Christian Urban <urbanc@in.tum.de> parents: 2205 diff changeset	16	\renewcommand{\isasymequiv}{$\dn$}
231a20534950 improved abstract, some tuning Christian Urban <urbanc@in.tum.de> parents: 2205 diff changeset	17	\renewcommand{\isasymemptyset}{$\varnothing$}
231a20534950 improved abstract, some tuning Christian Urban <urbanc@in.tum.de> parents: 2205 diff changeset	18
1975 b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	\begin{document}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	20
2032 5641981ec67d some preliminary notes of the abstract (qpaper); still need to see the motivating example Christian Urban <urbanc@in.tum.de> parents: 1975 diff changeset	21	\title{Quotients Revisited for Isabelle/HOL}
1975 b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	\author{Cezary Kaliszyk$^$ and Christian Urban$^$}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	\institute{$^*$ Technical University of Munich, Germany}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	\maketitle
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	25
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	26	\begin{abstract}
2213 231a20534950 improved abstract, some tuning Christian Urban <urbanc@in.tum.de> parents: 2205 diff changeset	27	Higher-order logic (HOL), used in several theorem provers, is based on a
231a20534950 improved abstract, some tuning Christian Urban <urbanc@in.tum.de> parents: 2205 diff changeset	28	small logic kernel, whose only mechanism for extension is the introduction
231a20534950 improved abstract, some tuning Christian Urban <urbanc@in.tum.de> parents: 2205 diff changeset	29	of safe definitions and non-empty types. Both extensions are often performed by
231a20534950 improved abstract, some tuning Christian Urban <urbanc@in.tum.de> parents: 2205 diff changeset	30	quotient constructions; for example finite sets are constructed by quotienting
2202 bdbf040dce89 first version of the abstract Christian Urban <urbanc@in.tum.de> parents: 2174 diff changeset	31	lists, or integers by quotienting pairs of natural numbers. To ease the work
2205 69b4eb4b12c6 added larry's quote Christian Urban <urbanc@in.tum.de> parents: 2202 diff changeset	32	involved with quotient constructions, we re-implemented in Isabelle/HOL
2202 bdbf040dce89 first version of the abstract Christian Urban <urbanc@in.tum.de> parents: 2174 diff changeset	33	the quotient package by Homeier. In doing so we extended his work
bdbf040dce89 first version of the abstract Christian Urban <urbanc@in.tum.de> parents: 2174 diff changeset	34	in order to deal with compositions of quotients. Also, we designed
bdbf040dce89 first version of the abstract Christian Urban <urbanc@in.tum.de> parents: 2174 diff changeset	35	our quotient package so that every step in a quotient construction
2213 231a20534950 improved abstract, some tuning Christian Urban <urbanc@in.tum.de> parents: 2205 diff changeset	36	can be performed separately. The importance to programming language research
231a20534950 improved abstract, some tuning Christian Urban <urbanc@in.tum.de> parents: 2205 diff changeset	37	is that many properties of programming languages are more convenient to verify
231a20534950 improved abstract, some tuning Christian Urban <urbanc@in.tum.de> parents: 2205 diff changeset	38	over $\alpha$-quotient terms, than over raw terms.
1975 b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	39	\end{abstract}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	40
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	41	% generated text of all theories
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	42	\input{session}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	43
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	44	% optional bibliography
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	45	\bibliographystyle{abbrv}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	46	\bibliography{root}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	47
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	48	\end{document}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	49
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	50	%%% Local Variables:
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	51	%%% mode: latex
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	52	%%% TeX-master: t
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper Christian Urban <urbanc@in.tum.de> parents: diff changeset	53	%%% End:

author	Christian Urban <urbanc@in.tum.de>
	Mon, 07 Jun 2010 11:33:00 +0200 (2010-06-07)
changeset 2213	231a20534950
parent 2205	69b4eb4b12c6
child 2214	02e03d4287ec
permissions	-rw-r--r--