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