src/HOL/Data_Structures/document/root.tex
author nipkow
Thu Mar 24 15:56:47 2016 +0100 (2016-03-24)
changeset 62706 49c6a54ceab6
parent 62496 f187aaf602c4
child 64318 1e92b5c35615
permissions -rw-r--r--
added Leftist_Heap
     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 
    31 For more details see \cite{Nipkow16}.
    32 \end{abstract}
    33 
    34 \setcounter{tocdepth}{1}
    35 \tableofcontents
    36 \newpage
    37 
    38 \input{session}
    39 
    40 \section{Bibliographic Notes}
    41 
    42 \paragraph{Red-black trees}
    43 The insert function follows Okasaki \cite{Okasaki}, the delete function
    44 Kahrs \cite{Kahrs-html,Kahrs-JFP01}.
    45 
    46 \paragraph{2-3 trees}
    47 Equational definitions were given by Hoffmann and
    48 O'Donnell~\cite{HoffmannOD-TOPLAS82} (only insertion)
    49 and Reade \cite{Reade-SCP92}.
    50 Our formalisation is based on the teaching material by
    51 Turbak~\cite{Turbak230} .
    52 
    53 \paragraph{1-2 brother trees}
    54 They were invented by Ottmann and Six~\cite{OttmannS76,OttmannW-CJ80}.
    55 The functional version is due to Hinze~\cite{Hinze-bro12}.
    56 
    57 \paragraph{AA trees}
    58 They were invented by Arne Anderson \cite{Andersson-WADS93}.
    59 Our formalisation follows Ragde~\cite{Ragde14} but fixes a number
    60 of mistakes.
    61 
    62 \paragraph{Splay trees}
    63 They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}.
    64 Our formalisation follows Schoenmakers \cite{Schoenmakers-IPL93}.
    65 
    66 \paragraph{Leftist heaps}
    67 They were invented by Crane \cite{Crane72}. A first functional implementation
    68 is due to N\'u\~{n}ez \emph{et al.}~\cite{NunezPP95}.
    69 
    70 \bibliographystyle{abbrv}
    71 \bibliography{root}
    72 
    73 \end{document}