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