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