src/HOL/Data_Structures/document/root.tex
author nipkow
Fri Oct 30 20:01:05 2015 +0100 (2015-10-30)
changeset 61525 87244a9cfe40
parent 61480 3885464e4874
child 61697 0753dd4c9144
permissions -rw-r--r--
added splay 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@61203
    30
\end{abstract}
nipkow@61203
    31
nipkow@61224
    32
\setcounter{tocdepth}{1}
nipkow@61203
    33
\tableofcontents
nipkow@61203
    34
\newpage
nipkow@61203
    35
nipkow@61203
    36
\input{session}
nipkow@61203
    37
nipkow@61224
    38
\section{Bibliographic Notes}
nipkow@61224
    39
nipkow@61480
    40
\paragraph{Red-black trees}
nipkow@61224
    41
The insert function follows Okasaki \cite{Okasaki}, the delete function
nipkow@61224
    42
Kahrs \cite{Kahrs-html,Kahrs-JFP01}.
nipkow@61224
    43
nipkow@61480
    44
\paragraph{2-3 trees}
nipkow@61480
    45
The function definitions are based on the teaching material by Franklyn Turbak.
nipkow@61480
    46
nipkow@61525
    47
\paragraph{Splay trees}
nipkow@61525
    48
They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}.
nipkow@61525
    49
Our formalisation follows Schoenmakers \cite{Schoenmakers-IPL93}.
nipkow@61525
    50
nipkow@61224
    51
\bibliographystyle{abbrv}
nipkow@61224
    52
\bibliography{root}
nipkow@61203
    53
nipkow@61203
    54
\end{document}