Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: root.tex Sprache: Latech

Original von: Isabelle^©

\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
% this should be the last package used
\usepackage{pdfsetup}

% snip
\newcommand{\repeatisanl}[1]{\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi}
\newcommand{\snip}[4]{\repeatisanl#2#4\repeatisanl#3}

\urlstyle{rm}
\isabellestyle{it}

\renewcommand{\isacharunderscore}{\_}
\renewcommand{\isacharunderscorekeyword}{\_}

% for uniform font size
\renewcommand{\isastyle}{\isastyleminor}

\begin{document}

\title{Functional Data Structures}
\author{Tobias Nipkow}
\maketitle

\begin{abstract}
A collection of verified functional data structures. The emphasis is on
conciseness of algorithms and succinctness of proofs, more in the style
of a textbook than a library of efficient algorithms.

For more details see \cite{Nipkow16}.
\end{abstract}

\setcounter{tocdepth}{1}
\tableofcontents
\newpage

\input{session}

\section{Bibliographic Notes}

\paragraph{Red-black trees}
The insert function follows Okasaki \cite{Okasaki}. The delete function
in theory \isa{RBT\_Set} follows Kahrs \cite{Kahrs-html,Kahrs-JFP01},
an alternative delete function is given in theory \isa{RBT\_Set2}.

\paragraph{2-3 trees}
Equational definitions were given by Hoffmann and
O'Donnell~\cite{HoffmannOD-TOPLAS82} (only insertion)
and Reade \cite{Reade-SCP92}.
Our formalisation is based on the teaching material by
Turbak~\cite{Turbak230} and the article by Hinze~\cite{jfp/Hinze18}.

\paragraph{1-2 brother trees}
They were invented by Ottmann and Six~\cite{OttmannS76,OttmannW-CJ80}.
The functional version is due to Hinze~\cite{Hinze-bro12}.

\paragraph{AA trees}
They were invented by Arne Anderson \cite{Andersson-WADS93}.
Our formalisation follows Ragde~\cite{Ragde14} but fixes a number
of mistakes.

\paragraph{Splay trees}
They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}.
Our formalisation follows Schoenmakers \cite{Schoenmakers-IPL93}.

\paragraph{Join-based BSTs}
They were invented by Adams \cite{Adams-TR92,Adams-JFP93}
and analyzed by Blelloch \emph{et al.} \cite{BlellochFS-SPAA16}.

\paragraph{Leftist heaps}
They were invented by Crane \cite{Crane72}. A first functional implementation
is due to N\'u\~{n}ez \emph{et al.}~\cite{NunezPP95}.

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.