author | nipkow |
Thu, 06 Aug 2020 17:39:57 +0200 | |
changeset 72100 | 9fa6dde8d959 |
parent 71352 | 41f3ca717da5 |
child 73404 | 299f6a8faccc |
permissions | -rw-r--r-- |
61203 | 1 |
\documentclass[11pt,a4paper]{article} |
2 |
\usepackage{isabelle,isabellesym} |
|
3 |
\usepackage{latexsym} |
|
64318
1e92b5c35615
Repaired LaTeX in HOL-Data_Structures
eberlm <eberlm@in.tum.de>
parents:
62706
diff
changeset
|
4 |
\usepackage{amssymb} |
1e92b5c35615
Repaired LaTeX in HOL-Data_Structures
eberlm <eberlm@in.tum.de>
parents:
62706
diff
changeset
|
5 |
\usepackage{amsmath} |
61203 | 6 |
% this should be the last package used |
7 |
\usepackage{pdfsetup} |
|
8 |
||
9 |
% snip |
|
10 |
\newcommand{\repeatisanl}[1]{\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi} |
|
11 |
\newcommand{\snip}[4]{\repeatisanl#2#4\repeatisanl#3} |
|
12 |
||
13 |
\urlstyle{rm} |
|
14 |
\isabellestyle{it} |
|
15 |
||
16 |
\renewcommand{\isacharunderscore}{\_} |
|
17 |
\renewcommand{\isacharunderscorekeyword}{\_} |
|
18 |
||
19 |
% for uniform font size |
|
20 |
\renewcommand{\isastyle}{\isastyleminor} |
|
21 |
||
22 |
\begin{document} |
|
23 |
||
24 |
\title{Functional Data Structures} |
|
25 |
\author{Tobias Nipkow} |
|
26 |
\maketitle |
|
27 |
||
28 |
\begin{abstract} |
|
29 |
A collection of verified functional data structures. The emphasis is on |
|
30 |
conciseness of algorithms and succinctness of proofs, more in the style |
|
31 |
of a textbook than a library of efficient algorithms. |
|
62496 | 32 |
|
33 |
For more details see \cite{Nipkow16}. |
|
61203 | 34 |
\end{abstract} |
35 |
||
61224 | 36 |
\setcounter{tocdepth}{1} |
61203 | 37 |
\tableofcontents |
38 |
\newpage |
|
39 |
||
40 |
\input{session} |
|
41 |
||
61224 | 42 |
\section{Bibliographic Notes} |
43 |
||
61480 | 44 |
\paragraph{Red-black trees} |
71352 | 45 |
The insert function follows Okasaki \cite{Okasaki}. The delete function |
46 |
in theory \isa{RBT\_Set} follows Kahrs \cite{Kahrs-html,Kahrs-JFP01}, |
|
47 |
an alternative delete function is given in theory \isa{RBT\_Set2}. |
|
61224 | 48 |
|
61480 | 49 |
\paragraph{2-3 trees} |
61791 | 50 |
Equational definitions were given by Hoffmann and |
51 |
O'Donnell~\cite{HoffmannOD-TOPLAS82} (only insertion) |
|
52 |
and Reade \cite{Reade-SCP92}. |
|
53 |
Our formalisation is based on the teaching material by |
|
72100 | 54 |
Turbak~\cite{Turbak230} and the article by Hinze~\cite{jfp/Hinze18}. |
61480 | 55 |
|
61784 | 56 |
\paragraph{1-2 brother trees} |
57 |
They were invented by Ottmann and Six~\cite{OttmannS76,OttmannW-CJ80}. |
|
58 |
The functional version is due to Hinze~\cite{Hinze-bro12}. |
|
59 |
||
62496 | 60 |
\paragraph{AA trees} |
61 |
They were invented by Arne Anderson \cite{Andersson-WADS93}. |
|
62 |
Our formalisation follows Ragde~\cite{Ragde14} but fixes a number |
|
63 |
of mistakes. |
|
64 |
||
61525 | 65 |
\paragraph{Splay trees} |
66 |
They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}. |
|
67 |
Our formalisation follows Schoenmakers \cite{Schoenmakers-IPL93}. |
|
68 |
||
67966
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
64318
diff
changeset
|
69 |
\paragraph{Join-based BSTs} |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
64318
diff
changeset
|
70 |
They were invented by Adams \cite{Adams-TR92,Adams-JFP93} |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
64318
diff
changeset
|
71 |
and analyzed by Blelloch \emph{et al.} \cite{BlellochFS-SPAA16}. |
f13796496e82
Added binary set operations with join-based implementation
nipkow
parents:
64318
diff
changeset
|
72 |
|
62706 | 73 |
\paragraph{Leftist heaps} |
74 |
They were invented by Crane \cite{Crane72}. A first functional implementation |
|
75 |
is due to N\'u\~{n}ez \emph{et al.}~\cite{NunezPP95}. |
|
76 |
||
61224 | 77 |
\bibliographystyle{abbrv} |
78 |
\bibliography{root} |
|
61203 | 79 |
|
80 |
\end{document} |