61203
|
1 |
\documentclass[11pt,a4paper]{article}
|
|
2 |
\usepackage{isabelle,isabellesym}
|
|
3 |
\usepackage{latexsym}
|
|
4 |
% this should be the last package used
|
|
5 |
\usepackage{pdfsetup}
|
|
6 |
|
|
7 |
% snip
|
|
8 |
\newcommand{\repeatisanl}[1]{\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi}
|
|
9 |
\newcommand{\snip}[4]{\repeatisanl#2#4\repeatisanl#3}
|
|
10 |
|
|
11 |
\urlstyle{rm}
|
|
12 |
\isabellestyle{it}
|
|
13 |
|
|
14 |
\renewcommand{\isacharunderscore}{\_}
|
|
15 |
\renewcommand{\isacharunderscorekeyword}{\_}
|
|
16 |
|
|
17 |
% for uniform font size
|
|
18 |
\renewcommand{\isastyle}{\isastyleminor}
|
|
19 |
|
|
20 |
\begin{document}
|
|
21 |
|
|
22 |
\title{Functional Data Structures}
|
|
23 |
\author{Tobias Nipkow}
|
|
24 |
\maketitle
|
|
25 |
|
|
26 |
\begin{abstract}
|
|
27 |
A collection of verified functional data structures. The emphasis is on
|
|
28 |
conciseness of algorithms and succinctness of proofs, more in the style
|
|
29 |
of a textbook than a library of efficient algorithms.
|
|
30 |
\end{abstract}
|
|
31 |
|
61224
|
32 |
\setcounter{tocdepth}{1}
|
61203
|
33 |
\tableofcontents
|
|
34 |
\newpage
|
|
35 |
|
|
36 |
\input{session}
|
|
37 |
|
61224
|
38 |
\section{Bibliographic Notes}
|
|
39 |
|
61480
|
40 |
\paragraph{Red-black trees}
|
61224
|
41 |
The insert function follows Okasaki \cite{Okasaki}, the delete function
|
|
42 |
Kahrs \cite{Kahrs-html,Kahrs-JFP01}.
|
|
43 |
|
61480
|
44 |
\paragraph{2-3 trees}
|
61791
|
45 |
Equational definitions were given by Hoffmann and
|
|
46 |
O'Donnell~\cite{HoffmannOD-TOPLAS82} (only insertion)
|
|
47 |
and Reade \cite{Reade-SCP92}.
|
|
48 |
Our formalisation is based on the teaching material by
|
|
49 |
Turbak~\cite{Turbak230} .
|
61480
|
50 |
|
61784
|
51 |
\paragraph{1-2 brother trees}
|
|
52 |
They were invented by Ottmann and Six~\cite{OttmannS76,OttmannW-CJ80}.
|
|
53 |
The functional version is due to Hinze~\cite{Hinze-bro12}.
|
|
54 |
|
61525
|
55 |
\paragraph{Splay trees}
|
|
56 |
They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}.
|
|
57 |
Our formalisation follows Schoenmakers \cite{Schoenmakers-IPL93}.
|
|
58 |
|
61224
|
59 |
\bibliographystyle{abbrv}
|
|
60 |
\bibliography{root}
|
61203
|
61 |
|
|
62 |
\end{document}
|